S553 · R1 ekran: kilit/durum/ayar ekranları system UI akış modeli

//! S553 models the controlled system-UI flow of the R1 phone target on top of
//! the retained scene abstraction (`crate::ui::scene`): a Lock scene, a Home
//! (status) scene, a Settings scene and a placeholder App scene, driven by an
//! explicit transition table over typed input events.
//!
//! The model covers: a constant-time 4-digit PIN compare with a bounded
//! attempt counter and a tick-based lockout, an unlock gesture that is only
//! honoured while the `PIN_REQUIRED` flag is clear, a bounded scene stack
//! (depth <= 4), a bounded settings store of `u8` flags, a status bar (battery
//! percent, signal bars 0..=5, HH:MM clock derived from a monotonic tick
//! count) and a `SceneReceipt` for every accepted event.  Every invalid
//! transition, out-of-range value, tick regression, arithmetic overflow,
//! stack overflow/underflow, out-of-order event id or divergent replay fails
//! closed and leaves the state untouched.  An exact replay of the last
//! accepted event is retained with the same receipt.
//!
//! This gate is a source/host model only.  It does not claim a panel, a touch
//! controller, a framebuffer, a modem, a board, a UART or any physical
//! observation, and it is not wired into any boot, IRQ, scheduler or driver
//! path.  The S540 and S543 physical verdicts stay immutable RED.
//! Predecessor: S552 (input focus and touch event routing model).  Next gate:
//! S554 (modem AT command transport framing model).

pub const S553_SEQUENCE: usize = 553;
pub const S553_EXPECTED_PREDECESSOR: usize = 552;
pub const S553_R1_STAGE: u8 = 2;
pub const S553_R1_RANGE_FIRST: usize = 536;
pub const S553_R1_RANGE_LAST: usize = 568;
pub const S553_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS: usize = 0;
pub const S553_PHYSICAL_OBSERVATIONS: usize = 0;
pub const S553_PHYSICAL_OR_DEVICE_OPERATIONS: usize = 0;
pub const S553_SD_WRITES: usize = 0;
pub const S553_UART_OPENS: usize = 0;
pub const S553_POWER_TRANSITIONS: usize = 0;
pub const S553_NEW_IMMUTABLE_RAW_CAPTURES: usize = 0;
pub const S553_S540_PHYSICAL_VERDICT_RETAINED_RED: bool = true;
pub const S553_S543_PHYSICAL_VERDICT_RETAINED_RED: bool = true;
pub const S553_AUTOMATIC_PROMOTION: bool = false;
pub const S553_BOOT_TO_UI_PHYSICALLY_OBSERVED: bool = false;
pub const S553_HARDWARE_PRESENT: bool = false;
pub const S553_R1_ACCEPTANCE_COMPLETE: bool = false;
pub const RUNBOOK_EXECUTED_IN_S553: bool = false;

/// Number of PIN digits; every digit must be in `0..=9`.
pub const S553_PIN_DIGITS: usize = 4;
/// Failed PIN attempts tolerated before a lockout; the sixth failure locks.
pub const S553_MAX_PIN_ATTEMPTS: u8 = 5;
/// Maximum scene stack depth (inclusive).
pub const S553_SCENE_STACK_MAX_DEPTH: usize = 4;
/// Number of `u8` flag slots in the settings store.
pub const S553_SETTINGS_CAPACITY: usize = 8;
/// Settings key of the `PIN_REQUIRED` flag (set by default).
pub const S553_SETTING_PIN_REQUIRED: u8 = 0;
/// Highest permitted signal bar count.
pub const S553_SIGNAL_BARS_MAX: u8 = 5;
/// Highest permitted battery percent.
pub const S553_BATTERY_PERCENT_MAX: u8 = 100;
/// Model tick rate: ticks per second of the monotonic tick counter.
pub const S553_TICK_HZ: u64 = 100;
/// Ticks per clock minute.
pub const S553_TICKS_PER_MINUTE: u64 = S553_TICK_HZ * 60;
/// Minutes per wall-clock day; the clock wraps at this boundary.
pub const S553_MINUTES_PER_DAY: u64 = 24 * 60;
/// Lockout duration after `S553_MAX_PIN_ATTEMPTS` is exceeded (30 s).
pub const S553_LOCKOUT_TICKS: u64 = 30 * S553_TICK_HZ;
/// Model default PIN used by `State::new()`; it is a fixture, not a secret.
pub const S553_DEFAULT_PIN: [u8; S553_PIN_DIGITS] = [1, 2, 3, 4];
/// Default settings flags: only `PIN_REQUIRED` set.
pub const S553_DEFAULT_SETTINGS: [u8; S553_SETTINGS_CAPACITY] = [1, 0, 0, 0, 0, 0, 0, 0];

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553Scene {
    Lock,
    Home,
    Settings,
    App,
}

impl G8lS553Scene {
    pub const fn index(self) -> u8 {
        match self {
            Self::Lock => 0,
            Self::Home => 1,
            Self::Settings => 2,
            Self::App => 3,
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553EventKind {
    UnlockGesture,
    PinEntry,
    Back,
    OpenSettings,
    OpenApp,
    ToggleSetting,
    Tick,
    BatteryReport,
    SignalReport,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553Input {
    UnlockGesture,
    PinEntry([u8; S553_PIN_DIGITS]),
    Back,
    OpenSettings,
    OpenApp,
    ToggleSetting(u8),
    Tick(u64),
    BatteryReport(u8),
    SignalReport(u8),
}

impl G8lS553Input {
    pub const fn kind(self) -> G8lS553EventKind {
        match self {
            Self::UnlockGesture => G8lS553EventKind::UnlockGesture,
            Self::PinEntry(_) => G8lS553EventKind::PinEntry,
            Self::Back => G8lS553EventKind::Back,
            Self::OpenSettings => G8lS553EventKind::OpenSettings,
            Self::OpenApp => G8lS553EventKind::OpenApp,
            Self::ToggleSetting(_) => G8lS553EventKind::ToggleSetting,
            Self::Tick(_) => G8lS553EventKind::Tick,
            Self::BatteryReport(_) => G8lS553EventKind::BatteryReport,
            Self::SignalReport(_) => G8lS553EventKind::SignalReport,
        }
    }

    const fn is_status_event(self) -> bool {
        matches!(
            self,
            Self::Tick(_) | Self::BatteryReport(_) | Self::SignalReport(_)
        )
    }
}

/// An input event with a contiguous, caller-assigned id (first id is 1).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS553InputEvent {
    pub id: u64,
    pub input: G8lS553Input,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS553StatusBar {
    pub battery_percent: u8,
    pub signal_bars: u8,
    pub clock_hour: u8,
    pub clock_minute: u8,
    pub clock_text: [u8; 5],
    pub tick_count: u64,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS553SceneReceipt {
    pub sequence: usize,
    pub predecessor_sequence: usize,
    pub transition_sequence: u64,
    pub event_id: u64,
    pub event_kind: G8lS553EventKind,
    pub from_scene: G8lS553Scene,
    pub to_scene: G8lS553Scene,
    pub stack: [G8lS553Scene; S553_SCENE_STACK_MAX_DEPTH],
    pub stack_depth: u8,
    pub status_bar: G8lS553StatusBar,
    pub settings: [u8; S553_SETTINGS_CAPACITY],
    pub pin_failed_attempts: u8,
    pub lockout_count: u8,
    pub locked_out: bool,
    pub lockout_release_tick: u64,
    pub hardware_present: bool,
    pub physical_observations: usize,
    pub runbook_executed: bool,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553SceneFlowOutcome {
    Transitioned(G8lS553SceneReceipt),
    StatusUpdated(G8lS553SceneReceipt),
    SettingToggled(G8lS553SceneReceipt),
    UnlockRejected(G8lS553SceneReceipt),
    LockedOut(G8lS553SceneReceipt),
    Retained(G8lS553SceneReceipt),
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553SceneFlowError {
    EventOrder,
    PublishedEventDivergence,
    InvalidTransition,
    SettingsFromLockForbidden,
    SceneStackOverflow,
    SceneStackUnderflow,
    PinRequired,
    PinDigitOutOfRange,
    LockedOut,
    SettingKeyOutOfRange,
    SettingValueNotFlag,
    BatteryOutOfRange,
    SignalOutOfRange,
    TickRegression,
    TickOverflow,
    TransitionCounterOverflow,
    LockoutCounterOverflow,
}

impl G8lS553SceneFlowError {
    pub const fn diagnostic_code(self) -> u64 {
        match self {
            Self::EventOrder => 1,
            Self::PublishedEventDivergence => 2,
            Self::InvalidTransition => 3,
            Self::SettingsFromLockForbidden => 4,
            Self::SceneStackOverflow => 5,
            Self::SceneStackUnderflow => 6,
            Self::PinRequired => 7,
            Self::PinDigitOutOfRange => 8,
            Self::LockedOut => 9,
            Self::SettingKeyOutOfRange => 10,
            Self::SettingValueNotFlag => 11,
            Self::BatteryOutOfRange => 12,
            Self::SignalOutOfRange => 13,
            Self::TickRegression => 14,
            Self::TickOverflow => 15,
            Self::TransitionCounterOverflow => 16,
            Self::LockoutCounterOverflow => 17,
        }
    }
}

/// What an accepted scene event does to the scene stack.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS553TransitionAction {
    /// Lock -> Home; resets the stack to `[Home]`.
    Unlock,
    /// Push the given scene (bounded by `S553_SCENE_STACK_MAX_DEPTH`).
    Push(G8lS553Scene),
    /// Pop the top scene; the stack must keep at least one scene.
    Pop,
    /// Home -> Lock; resets the stack to `[Lock]`.
    Lock,
    /// Scene unchanged (settings toggle).
    Stay,
    /// Explicit guard rejection.
    Reject(G8lS553SceneFlowError),
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS553TransitionRule {
    pub from: G8lS553Scene,
    pub kind: G8lS553EventKind,
    pub action: G8lS553TransitionAction,
}

const fn rule(
    from: G8lS553Scene,
    kind: G8lS553EventKind,
    action: G8lS553TransitionAction,
) -> G8lS553TransitionRule {
    G8lS553TransitionRule { from, kind, action }
}

/// Explicit scene transition table.  Status events (tick/battery/signal) are
/// accepted in every scene and are not part of this table.  Any
/// (scene, kind) pair absent from the table is an invalid transition.
pub const S553_TRANSITION_TABLE: [G8lS553TransitionRule; 11] = [
    rule(
        G8lS553Scene::Lock,
        G8lS553EventKind::UnlockGesture,
        G8lS553TransitionAction::Unlock,
    ),
    rule(
        G8lS553Scene::Lock,
        G8lS553EventKind::PinEntry,
        G8lS553TransitionAction::Unlock,
    ),
    rule(
        G8lS553Scene::Lock,
        G8lS553EventKind::OpenSettings,
        G8lS553TransitionAction::Reject(G8lS553SceneFlowError::SettingsFromLockForbidden),
    ),
    rule(
        G8lS553Scene::Home,
        G8lS553EventKind::OpenSettings,
        G8lS553TransitionAction::Push(G8lS553Scene::Settings),
    ),
    rule(
        G8lS553Scene::Home,
        G8lS553EventKind::OpenApp,
        G8lS553TransitionAction::Push(G8lS553Scene::App),
    ),
    rule(
        G8lS553Scene::Home,
        G8lS553EventKind::Back,
        G8lS553TransitionAction::Lock,
    ),
    rule(
        G8lS553Scene::Settings,
        G8lS553EventKind::ToggleSetting,
        G8lS553TransitionAction::Stay,
    ),
    rule(
        G8lS553Scene::Settings,
        G8lS553EventKind::Back,
        G8lS553TransitionAction::Pop,
    ),
    rule(
        G8lS553Scene::Settings,
        G8lS553EventKind::OpenApp,
        G8lS553TransitionAction::Push(G8lS553Scene::App),
    ),
    rule(
        G8lS553Scene::App,
        G8lS553EventKind::Back,
        G8lS553TransitionAction::Pop,
    ),
    rule(
        G8lS553Scene::App,
        G8lS553EventKind::OpenSettings,
        G8lS553TransitionAction::Push(G8lS553Scene::Settings),
    ),
];

pub fn s553_lookup_transition(
    from: G8lS553Scene,
    kind: G8lS553EventKind,
) -> Option<G8lS553TransitionAction> {
    S553_TRANSITION_TABLE
        .iter()
        .find(|entry| entry.from == from && entry.kind == kind)
        .map(|entry| entry.action)
}

/// Constant-time PIN compare: every digit is examined and OR-accumulated so
/// the result does not depend on the position of the first mismatch.
pub fn s553_pin_matches_constant_time(
    entered: [u8; S553_PIN_DIGITS],
    expected: [u8; S553_PIN_DIGITS],
) -> bool {
    let mut difference: u8 = 0;
    let mut index = 0;
    while index < S553_PIN_DIGITS {
        difference |= entered[index] ^ expected[index];
        index += 1;
    }
    difference == 0
}

pub fn s553_pin_digits_are_valid(pin: [u8; S553_PIN_DIGITS]) -> bool {
    pin.iter().all(|digit| *digit <= 9)
}

/// Derives the HH:MM wall clock from a monotonic tick count; the clock wraps
/// every `S553_MINUTES_PER_DAY` minutes.
pub const fn s553_clock_from_ticks(tick_count: u64) -> (u8, u8) {
    let minute_of_day = (tick_count / S553_TICKS_PER_MINUTE) % S553_MINUTES_PER_DAY;
    ((minute_of_day / 60) as u8, (minute_of_day % 60) as u8)
}

/// Encodes HH:MM as five ASCII bytes.
pub const fn s553_clock_text(hour: u8, minute: u8) -> [u8; 5] {
    [
        b'0' + hour / 10,
        b'0' + hour % 10,
        b':',
        b'0' + minute / 10,
        b'0' + minute % 10,
    ]
}

const fn status_bar(battery_percent: u8, signal_bars: u8, tick_count: u64) -> G8lS553StatusBar {
    let (clock_hour, clock_minute) = s553_clock_from_ticks(tick_count);
    G8lS553StatusBar {
        battery_percent,
        signal_bars,
        clock_hour,
        clock_minute,
        clock_text: s553_clock_text(clock_hour, clock_minute),
        tick_count,
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Snapshot {
    stack: [G8lS553Scene; S553_SCENE_STACK_MAX_DEPTH],
    depth: u8,
    status: G8lS553StatusBar,
    settings: [u8; S553_SETTINGS_CAPACITY],
    pin_failed_attempts: u8,
    lockout_count: u8,
    lockout_release_tick: Option<u64>,
    transitions: u64,
}

impl Snapshot {
    const fn current_scene(&self) -> G8lS553Scene {
        self.stack[(self.depth as usize).saturating_sub(1)]
    }

    const fn locked_out(&self) -> bool {
        self.lockout_release_tick.is_some()
    }
}

#[derive(Debug)]
pub struct G8lS553SystemUiState {
    pin: [u8; S553_PIN_DIGITS],
    snapshot: Snapshot,
    last: Option<(G8lS553InputEvent, G8lS553SceneReceipt)>,
}

impl G8lS553SystemUiState {
    pub const fn new() -> Self {
        Self {
            pin: S553_DEFAULT_PIN,
            snapshot: Snapshot {
                stack: [G8lS553Scene::Lock; S553_SCENE_STACK_MAX_DEPTH],
                depth: 1,
                status: status_bar(0, 0, 0),
                settings: S553_DEFAULT_SETTINGS,
                pin_failed_attempts: 0,
                lockout_count: 0,
                lockout_release_tick: None,
                transitions: 0,
            },
            last: None,
        }
    }

    /// Builds a state with a caller-provided PIN; digits must be `0..=9`.
    pub fn with_pin(pin: [u8; S553_PIN_DIGITS]) -> Result<Self, G8lS553SceneFlowError> {
        if !s553_pin_digits_are_valid(pin) {
            return Err(G8lS553SceneFlowError::PinDigitOutOfRange);
        }
        let mut state = Self::new();
        state.pin = pin;
        Ok(state)
    }

    pub const fn current_scene(&self) -> G8lS553Scene {
        self.snapshot.current_scene()
    }

    pub const fn stack_depth(&self) -> usize {
        self.snapshot.depth as usize
    }

    pub const fn status_bar(&self) -> G8lS553StatusBar {
        self.snapshot.status
    }

    pub const fn settings(&self) -> [u8; S553_SETTINGS_CAPACITY] {
        self.snapshot.settings
    }

    pub const fn pin_failed_attempts(&self) -> u8 {
        self.snapshot.pin_failed_attempts
    }

    pub const fn lockout_count(&self) -> u8 {
        self.snapshot.lockout_count
    }

    pub const fn locked_out(&self) -> bool {
        self.snapshot.locked_out()
    }

    pub const fn accepted_events(&self) -> u64 {
        self.snapshot.transitions
    }

    /// Id the next new event must carry.
    pub const fn expected_event_id(&self) -> u64 {
        self.snapshot.transitions + 1
    }

    pub fn last_receipt(&self) -> Option<G8lS553SceneReceipt> {
        self.last.map(|(_, receipt)| receipt)
    }
}

impl Default for G8lS553SystemUiState {
    fn default() -> Self {
        Self::new()
    }
}

fn receipt_for(
    event: G8lS553InputEvent,
    from_scene: G8lS553Scene,
    next: &Snapshot,
) -> G8lS553SceneReceipt {
    G8lS553SceneReceipt {
        sequence: S553_SEQUENCE,
        predecessor_sequence: S553_EXPECTED_PREDECESSOR,
        transition_sequence: next.transitions,
        event_id: event.id,
        event_kind: event.input.kind(),
        from_scene,
        to_scene: next.current_scene(),
        stack: next.stack,
        stack_depth: next.depth,
        status_bar: next.status,
        settings: next.settings,
        pin_failed_attempts: next.pin_failed_attempts,
        lockout_count: next.lockout_count,
        locked_out: next.locked_out(),
        lockout_release_tick: next.lockout_release_tick.unwrap_or(0),
        hardware_present: S553_HARDWARE_PRESENT,
        physical_observations: S553_PHYSICAL_OBSERVATIONS,
        runbook_executed: RUNBOOK_EXECUTED_IN_S553,
    }
}

fn apply_status_event(
    next: &mut Snapshot,
    input: G8lS553Input,
) -> Result<(), G8lS553SceneFlowError> {
    match input {
        G8lS553Input::Tick(tick_count) => {
            if tick_count < next.status.tick_count {
                return Err(G8lS553SceneFlowError::TickRegression);
            }
            next.status = status_bar(
                next.status.battery_percent,
                next.status.signal_bars,
                tick_count,
            );
            if let Some(release) = next.lockout_release_tick {
                if tick_count >= release {
                    next.lockout_release_tick = None;
                }
            }
        }
        G8lS553Input::BatteryReport(percent) => {
            if percent > S553_BATTERY_PERCENT_MAX {
                return Err(G8lS553SceneFlowError::BatteryOutOfRange);
            }
            next.status = status_bar(percent, next.status.signal_bars, next.status.tick_count);
        }
        G8lS553Input::SignalReport(bars) => {
            if bars > S553_SIGNAL_BARS_MAX {
                return Err(G8lS553SceneFlowError::SignalOutOfRange);
            }
            next.status = status_bar(next.status.battery_percent, bars, next.status.tick_count);
        }
        _ => return Err(G8lS553SceneFlowError::InvalidTransition),
    }
    Ok(())
}

fn push_scene(next: &mut Snapshot, scene: G8lS553Scene) -> Result<(), G8lS553SceneFlowError> {
    let depth = next.depth as usize;
    if depth >= S553_SCENE_STACK_MAX_DEPTH {
        return Err(G8lS553SceneFlowError::SceneStackOverflow);
    }
    next.stack[depth] = scene;
    next.depth = next
        .depth
        .checked_add(1)
        .ok_or(G8lS553SceneFlowError::SceneStackOverflow)?;
    Ok(())
}

fn pop_scene(next: &mut Snapshot) -> Result<(), G8lS553SceneFlowError> {
    if next.depth <= 1 {
        return Err(G8lS553SceneFlowError::SceneStackUnderflow);
    }
    next.depth -= 1;
    next.stack[next.depth as usize] = G8lS553Scene::Lock;
    Ok(())
}

fn reset_stack(next: &mut Snapshot, base: G8lS553Scene) {
    next.stack = [G8lS553Scene::Lock; S553_SCENE_STACK_MAX_DEPTH];
    next.stack[0] = base;
    next.depth = 1;
}

/// Result of an unlock attempt on the scene stack.
enum Unlock {
    Granted,
    Rejected,
    LockedOut,
}

fn apply_unlock(
    next: &mut Snapshot,
    pin: [u8; S553_PIN_DIGITS],
    input: G8lS553Input,
) -> Result<Unlock, G8lS553SceneFlowError> {
    if next.locked_out() {
        return Err(G8lS553SceneFlowError::LockedOut);
    }
    let entered = match input {
        G8lS553Input::UnlockGesture => {
            if next.settings[S553_SETTING_PIN_REQUIRED as usize] != 0 {
                return Err(G8lS553SceneFlowError::PinRequired);
            }
            next.pin_failed_attempts = 0;
            reset_stack(next, G8lS553Scene::Home);
            return Ok(Unlock::Granted);
        }
        G8lS553Input::PinEntry(entered) => entered,
        _ => return Err(G8lS553SceneFlowError::InvalidTransition),
    };
    if !s553_pin_digits_are_valid(entered) {
        return Err(G8lS553SceneFlowError::PinDigitOutOfRange);
    }
    if s553_pin_matches_constant_time(entered, pin) {
        next.pin_failed_attempts = 0;
        reset_stack(next, G8lS553Scene::Home);
        return Ok(Unlock::Granted);
    }
    let attempts = next
        .pin_failed_attempts
        .checked_add(1)
        .ok_or(G8lS553SceneFlowError::LockoutCounterOverflow)?;
    if attempts > S553_MAX_PIN_ATTEMPTS {
        let release = next
            .status
            .tick_count
            .checked_add(S553_LOCKOUT_TICKS)
            .ok_or(G8lS553SceneFlowError::TickOverflow)?;
        next.lockout_count = next
            .lockout_count
            .checked_add(1)
            .ok_or(G8lS553SceneFlowError::LockoutCounterOverflow)?;
        next.lockout_release_tick = Some(release);
        next.pin_failed_attempts = 0;
        return Ok(Unlock::LockedOut);
    }
    next.pin_failed_attempts = attempts;
    Ok(Unlock::Rejected)
}

fn apply_toggle(next: &mut Snapshot, key: u8) -> Result<(), G8lS553SceneFlowError> {
    if key as usize >= S553_SETTINGS_CAPACITY {
        return Err(G8lS553SceneFlowError::SettingKeyOutOfRange);
    }
    let value = next.settings[key as usize];
    if value > 1 {
        return Err(G8lS553SceneFlowError::SettingValueNotFlag);
    }
    next.settings[key as usize] = value ^ 1;
    Ok(())
}

/// Drives one input event through the scene flow.  Fail-closed: any `Err`
/// leaves the state untouched and does not consume the event id.  An exact
/// replay of the last accepted event is retained with the same receipt; a
/// different payload under the last accepted id is a divergence.
pub fn service_s553_model_scene_flow(
    state: &mut G8lS553SystemUiState,
    event: G8lS553InputEvent,
) -> Result<G8lS553SceneFlowOutcome, G8lS553SceneFlowError> {
    if let Some((published_event, published_receipt)) = state.last {
        if event.id == published_event.id {
            if event == published_event {
                return Ok(G8lS553SceneFlowOutcome::Retained(published_receipt));
            }
            return Err(G8lS553SceneFlowError::PublishedEventDivergence);
        }
    }
    if event.id != state.expected_event_id() {
        return Err(G8lS553SceneFlowError::EventOrder);
    }

    let mut next = state.snapshot;
    next.transitions = next
        .transitions
        .checked_add(1)
        .ok_or(G8lS553SceneFlowError::TransitionCounterOverflow)?;
    let from_scene = next.current_scene();

    let outcome: fn(G8lS553SceneReceipt) -> G8lS553SceneFlowOutcome =
        if event.input.is_status_event() {
            apply_status_event(&mut next, event.input)?;
            G8lS553SceneFlowOutcome::StatusUpdated
        } else {
            let action = s553_lookup_transition(from_scene, event.input.kind())
                .ok_or(G8lS553SceneFlowError::InvalidTransition)?;
            match action {
                G8lS553TransitionAction::Reject(error) => return Err(error),
                G8lS553TransitionAction::Unlock => {
                    match apply_unlock(&mut next, state.pin, event.input)? {
                        Unlock::Granted => G8lS553SceneFlowOutcome::Transitioned,
                        Unlock::Rejected => G8lS553SceneFlowOutcome::UnlockRejected,
                        Unlock::LockedOut => G8lS553SceneFlowOutcome::LockedOut,
                    }
                }
                G8lS553TransitionAction::Push(scene) => {
                    push_scene(&mut next, scene)?;
                    G8lS553SceneFlowOutcome::Transitioned
                }
                G8lS553TransitionAction::Pop => {
                    pop_scene(&mut next)?;
                    G8lS553SceneFlowOutcome::Transitioned
                }
                G8lS553TransitionAction::Lock => {
                    reset_stack(&mut next, G8lS553Scene::Lock);
                    G8lS553SceneFlowOutcome::Transitioned
                }
                G8lS553TransitionAction::Stay => match event.input {
                    G8lS553Input::ToggleSetting(key) => {
                        apply_toggle(&mut next, key)?;
                        G8lS553SceneFlowOutcome::SettingToggled
                    }
                    _ => return Err(G8lS553SceneFlowError::InvalidTransition),
                },
            }
        };

    let receipt = receipt_for(event, from_scene, &next);
    state.snapshot = next;
    state.last = Some((event, receipt));
    Ok(outcome(receipt))
}

use aselsan_microkernel_simulation::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s553_r1_system_ui_lock_status_settings_scene_flow_model::*;
use std::collections::BTreeSet;

const SOURCE: &str = include_str!(
    "../../kernel/src/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s553_r1_system_ui_lock_status_settings_scene_flow_model.rs"
);
const MAIN: &str = include_str!("../../kernel/src/main.rs");
const SIMULATION_LIB: &str = include_str!("../src/lib.rs");

type Outcome = G8lS553SceneFlowOutcome;
type Error = G8lS553SceneFlowError;
type Scene = G8lS553Scene;
type Input = G8lS553Input;

fn event(id: u64, input: Input) -> G8lS553InputEvent {
    G8lS553InputEvent { id, input }
}

/// Drives the next event using the state's expected id.
fn drive(state: &mut G8lS553SystemUiState, input: Input) -> Result<Outcome, Error> {
    let id = state.expected_event_id();
    service_s553_model_scene_flow(state, event(id, input))
}

fn receipt_of(outcome: Outcome) -> G8lS553SceneReceipt {
    match outcome {
        Outcome::Transitioned(receipt)
        | Outcome::StatusUpdated(receipt)
        | Outcome::SettingToggled(receipt)
        | Outcome::UnlockRejected(receipt)
        | Outcome::LockedOut(receipt)
        | Outcome::Retained(receipt) => receipt,
    }
}

fn unlocked_home() -> G8lS553SystemUiState {
    let mut state = G8lS553SystemUiState::new();
    let outcome = drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)).unwrap();
    assert!(matches!(outcome, Outcome::Transitioned(_)));
    assert_eq!(state.current_scene(), Scene::Home);
    state
}

#[test]
fn sequence_scope_and_nonpromotion_are_exact() {
    assert_eq!(S553_SEQUENCE, 553);
    assert_eq!(S553_EXPECTED_PREDECESSOR, 552);
    assert_eq!(S553_R1_STAGE, 2);
    assert_eq!(S553_R1_RANGE_FIRST, 536);
    assert_eq!(S553_R1_RANGE_LAST, 568);
    assert_eq!(S553_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS, 0);
    assert_eq!(S553_PHYSICAL_OBSERVATIONS, 0);
    assert_eq!(S553_PHYSICAL_OR_DEVICE_OPERATIONS, 0);
    assert_eq!(S553_SD_WRITES, 0);
    assert_eq!(S553_UART_OPENS, 0);
    assert_eq!(S553_POWER_TRANSITIONS, 0);
    assert_eq!(S553_NEW_IMMUTABLE_RAW_CAPTURES, 0);
    assert!(S553_S540_PHYSICAL_VERDICT_RETAINED_RED);
    assert!(S553_S543_PHYSICAL_VERDICT_RETAINED_RED);
    assert!(!S553_AUTOMATIC_PROMOTION);
    assert!(!S553_BOOT_TO_UI_PHYSICALLY_OBSERVED);
    assert!(!S553_HARDWARE_PRESENT);
    assert!(!S553_R1_ACCEPTANCE_COMPLETE);
    assert!(!RUNBOOK_EXECUTED_IN_S553);
    assert_eq!(S553_PIN_DIGITS, 4);
    assert_eq!(S553_MAX_PIN_ATTEMPTS, 5);
    assert_eq!(S553_SCENE_STACK_MAX_DEPTH, 4);
    assert_eq!(S553_SETTINGS_CAPACITY, 8);
    assert_eq!(S553_SIGNAL_BARS_MAX, 5);
    assert_eq!(S553_BATTERY_PERCENT_MAX, 100);
    assert_eq!(S553_TICKS_PER_MINUTE, 6_000);
    assert_eq!(S553_LOCKOUT_TICKS, 3_000);
}

#[test]
fn module_is_registered_in_kernel_and_simulation() {
    let module = "g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s553_r1_system_ui_lock_status_settings_scene_flow_model";
    assert!(MAIN.contains(&format!("mod {module};")));
    assert!(SIMULATION_LIB.contains(&format!("pub mod {module};")));
}

#[test]
fn source_has_no_device_execution_or_uart_emission_surface() {
    for forbidden in [
        "unsafe",
        "asm!",
        "write_volatile",
        "crate::uart",
        "crate::arch",
        "#[no_mangle]",
        "spin::",
        "std::",
        "kprintln!",
    ] {
        assert!(!SOURCE.contains(forbidden), "forbidden token: {forbidden}");
    }
    assert!(SOURCE.contains("source/host model only"));
    assert!(SOURCE.contains("S553_HARDWARE_PRESENT: bool = false"));
    assert!(SOURCE.contains("S553_PHYSICAL_OBSERVATIONS: usize = 0"));
    assert!(SOURCE.contains("S553_R1_ACCEPTANCE_COMPLETE: bool = false"));
    assert!(SOURCE.contains("RUNBOOK_EXECUTED_IN_S553: bool = false"));
}

#[test]
fn diagnostic_codes_are_nonzero_and_unique() {
    let errors = [
        Error::EventOrder,
        Error::PublishedEventDivergence,
        Error::InvalidTransition,
        Error::SettingsFromLockForbidden,
        Error::SceneStackOverflow,
        Error::SceneStackUnderflow,
        Error::PinRequired,
        Error::PinDigitOutOfRange,
        Error::LockedOut,
        Error::SettingKeyOutOfRange,
        Error::SettingValueNotFlag,
        Error::BatteryOutOfRange,
        Error::SignalOutOfRange,
        Error::TickRegression,
        Error::TickOverflow,
        Error::TransitionCounterOverflow,
        Error::LockoutCounterOverflow,
    ];
    let codes: BTreeSet<_> = errors.into_iter().map(Error::diagnostic_code).collect();
    assert_eq!(codes.len(), errors.len());
    assert!(!codes.contains(&0));
}

#[test]
fn exact_replay_retains_the_same_receipt() {
    let mut state = G8lS553SystemUiState::new();
    let first = event(1, Input::PinEntry(S553_DEFAULT_PIN));
    let Outcome::Transitioned(receipt) = service_s553_model_scene_flow(&mut state, first).unwrap()
    else {
        panic!("first unlock must transition")
    };
    assert_eq!(
        service_s553_model_scene_flow(&mut state, first),
        Ok(Outcome::Retained(receipt))
    );
    assert_eq!(state.accepted_events(), 1);
    assert_eq!(state.expected_event_id(), 2);
    assert_eq!(state.last_receipt(), Some(receipt));
}

#[test]
fn divergent_input_after_publication_fails_closed() {
    let mut state = G8lS553SystemUiState::new();
    service_s553_model_scene_flow(&mut state, event(1, Input::PinEntry(S553_DEFAULT_PIN))).unwrap();
    let before = state.last_receipt();
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(1, Input::UnlockGesture)),
        Err(Error::PublishedEventDivergence)
    );
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(1, Input::PinEntry([1, 2, 3, 5]))),
        Err(Error::PublishedEventDivergence)
    );
    assert_eq!(state.last_receipt(), before);
    assert_eq!(state.current_scene(), Scene::Home);
}

#[test]
fn default_state_starts_locked_with_pin_required() {
    let state = G8lS553SystemUiState::new();
    assert_eq!(state.current_scene(), Scene::Lock);
    assert_eq!(state.stack_depth(), 1);
    assert_eq!(state.settings(), S553_DEFAULT_SETTINGS);
    assert_eq!(state.settings()[S553_SETTING_PIN_REQUIRED as usize], 1);
    assert_eq!(state.pin_failed_attempts(), 0);
    assert_eq!(state.lockout_count(), 0);
    assert!(!state.locked_out());
    assert_eq!(state.accepted_events(), 0);
    assert_eq!(state.expected_event_id(), 1);
    assert_eq!(state.last_receipt(), None);
    let status = state.status_bar();
    assert_eq!(status.battery_percent, 0);
    assert_eq!(status.signal_bars, 0);
    assert_eq!(status.clock_text, *b"00:00");
    assert_eq!(status.tick_count, 0);
    let default_state = G8lS553SystemUiState::default();
    assert_eq!(default_state.current_scene(), Scene::Lock);
    assert_eq!(default_state.settings(), S553_DEFAULT_SETTINGS);
}

#[test]
fn correct_pin_unlocks_to_home_with_exact_receipt() {
    let mut state = G8lS553SystemUiState::new();
    drive(&mut state, Input::PinEntry([1, 2, 3, 5])).unwrap();
    assert_eq!(state.pin_failed_attempts(), 1);
    let Outcome::Transitioned(receipt) = drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)).unwrap()
    else {
        panic!("correct PIN must unlock")
    };
    assert_eq!(receipt.sequence, 553);
    assert_eq!(receipt.predecessor_sequence, 552);
    assert_eq!(receipt.transition_sequence, 2);
    assert_eq!(receipt.event_id, 2);
    assert_eq!(receipt.event_kind, G8lS553EventKind::PinEntry);
    assert_eq!(receipt.from_scene, Scene::Lock);
    assert_eq!(receipt.to_scene, Scene::Home);
    assert_eq!(receipt.stack_depth, 1);
    assert_eq!(receipt.stack[0], Scene::Home);
    assert_eq!(receipt.pin_failed_attempts, 0);
    assert_eq!(receipt.lockout_count, 0);
    assert!(!receipt.locked_out);
    assert_eq!(receipt.lockout_release_tick, 0);
    assert!(!receipt.hardware_present);
    assert_eq!(receipt.physical_observations, 0);
    assert!(!receipt.runbook_executed);
    assert_eq!(state.current_scene(), Scene::Home);
}

#[test]
fn unlock_gesture_requires_pin_flag_cleared() {
    let mut state = G8lS553SystemUiState::new();
    assert_eq!(drive(&mut state, Input::UnlockGesture), Err(Error::PinRequired));
    assert_eq!(state.current_scene(), Scene::Lock);
    assert_eq!(state.accepted_events(), 0);

    drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)).unwrap();
    drive(&mut state, Input::OpenSettings).unwrap();
    let Outcome::SettingToggled(receipt) =
        drive(&mut state, Input::ToggleSetting(S553_SETTING_PIN_REQUIRED)).unwrap()
    else {
        panic!("toggle must be accepted in Settings")
    };
    assert_eq!(receipt.settings[0], 0);
    assert_eq!(receipt.to_scene, Scene::Settings);
    drive(&mut state, Input::Back).unwrap();
    assert_eq!(state.current_scene(), Scene::Home);
    drive(&mut state, Input::Back).unwrap();
    assert_eq!(state.current_scene(), Scene::Lock);
    let Outcome::Transitioned(receipt) = drive(&mut state, Input::UnlockGesture).unwrap() else {
        panic!("gesture must unlock once PIN_REQUIRED is clear")
    };
    assert_eq!(receipt.event_kind, G8lS553EventKind::UnlockGesture);
    assert_eq!(receipt.to_scene, Scene::Home);
    assert_eq!(receipt.transition_sequence, 6);
}

#[test]
fn sixth_pin_failure_locks_out_and_increments_lockout_counter() {
    let mut state = G8lS553SystemUiState::new();
    for attempt in 1..=S553_MAX_PIN_ATTEMPTS {
        let Outcome::UnlockRejected(receipt) = drive(&mut state, Input::PinEntry([9, 9, 9, 9])).unwrap()
        else {
            panic!("wrong PIN must be rejected without lockout")
        };
        assert_eq!(receipt.pin_failed_attempts, attempt);
        assert_eq!(receipt.to_scene, Scene::Lock);
        assert!(!receipt.locked_out);
    }
    let Outcome::LockedOut(receipt) = drive(&mut state, Input::PinEntry([9, 9, 9, 9])).unwrap() else {
        panic!("sixth failure must lock out")
    };
    assert!(receipt.locked_out);
    assert_eq!(receipt.lockout_count, 1);
    assert_eq!(receipt.pin_failed_attempts, 0);
    assert_eq!(receipt.lockout_release_tick, S553_LOCKOUT_TICKS);
    assert!(state.locked_out());
    assert_eq!(state.lockout_count(), 1);
}

#[test]
fn lockout_rejects_pins_until_release_tick() {
    let mut state = G8lS553SystemUiState::new();
    drive(&mut state, Input::Tick(1_000)).unwrap();
    for _ in 0..=S553_MAX_PIN_ATTEMPTS {
        drive(&mut state, Input::PinEntry([0, 0, 0, 0])).unwrap();
    }
    assert!(state.locked_out());
    assert_eq!(state.last_receipt().unwrap().lockout_release_tick, 1_000 + S553_LOCKOUT_TICKS);
    assert_eq!(drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)), Err(Error::LockedOut));
    assert_eq!(drive(&mut state, Input::UnlockGesture), Err(Error::LockedOut));
    drive(&mut state, Input::Tick(1_000 + S553_LOCKOUT_TICKS - 1)).unwrap();
    assert!(state.locked_out());
    assert_eq!(drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)), Err(Error::LockedOut));
    let Outcome::StatusUpdated(receipt) = drive(&mut state, Input::Tick(1_000 + S553_LOCKOUT_TICKS)).unwrap()
    else {
        panic!("tick must be a status update")
    };
    assert!(!receipt.locked_out);
    assert_eq!(receipt.lockout_release_tick, 0);
    assert!(matches!(
        drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)),
        Ok(Outcome::Transitioned(_))
    ));
    assert_eq!(state.current_scene(), Scene::Home);
}

#[test]
fn settings_are_unreachable_from_lock() {
    let mut state = G8lS553SystemUiState::new();
    assert_eq!(drive(&mut state, Input::OpenSettings), Err(Error::SettingsFromLockForbidden));
    assert_eq!(drive(&mut state, Input::OpenApp), Err(Error::InvalidTransition));
    assert_eq!(drive(&mut state, Input::Back), Err(Error::InvalidTransition));
    assert_eq!(drive(&mut state, Input::ToggleSetting(1)), Err(Error::InvalidTransition));
    assert_eq!(state.current_scene(), Scene::Lock);
    assert_eq!(state.accepted_events(), 0);
    assert_eq!(
        s553_lookup_transition(Scene::Lock, G8lS553EventKind::OpenSettings),
        Some(G8lS553TransitionAction::Reject(Error::SettingsFromLockForbidden))
    );
}

#[test]
fn scene_stack_depth_is_bounded_at_four() {
    let mut state = unlocked_home();
    drive(&mut state, Input::OpenSettings).unwrap();
    drive(&mut state, Input::OpenApp).unwrap();
    let Outcome::Transitioned(receipt) = drive(&mut state, Input::OpenSettings).unwrap() else {
        panic!("fourth push must be accepted")
    };
    assert_eq!(receipt.stack_depth, 4);
    assert_eq!(
        receipt.stack,
        [Scene::Home, Scene::Settings, Scene::App, Scene::Settings]
    );
    assert_eq!(drive(&mut state, Input::OpenApp), Err(Error::SceneStackOverflow));
    assert_eq!(state.stack_depth(), 4);
    assert_eq!(state.current_scene(), Scene::Settings);
    assert_eq!(state.accepted_events(), 4);
}

#[test]
fn back_pops_scenes_and_home_back_locks_the_device() {
    let mut state = unlocked_home();
    drive(&mut state, Input::OpenApp).unwrap();
    drive(&mut state, Input::OpenSettings).unwrap();
    let Outcome::Transitioned(receipt) = drive(&mut state, Input::Back).unwrap() else {
        panic!("back must pop")
    };
    assert_eq!(receipt.from_scene, Scene::Settings);
    assert_eq!(receipt.to_scene, Scene::App);
    assert_eq!(receipt.stack_depth, 2);
    assert_eq!(receipt.stack[2], Scene::Lock);
    drive(&mut state, Input::Back).unwrap();
    assert_eq!(state.current_scene(), Scene::Home);
    let Outcome::Transitioned(receipt) = drive(&mut state, Input::Back).unwrap() else {
        panic!("home back must lock")
    };
    assert_eq!(receipt.from_scene, Scene::Home);
    assert_eq!(receipt.to_scene, Scene::Lock);
    assert_eq!(receipt.stack_depth, 1);
    assert_eq!(receipt.stack[0], Scene::Lock);
    assert_eq!(drive(&mut state, Input::Back), Err(Error::InvalidTransition));
}

#[test]
fn toggle_setting_flips_flags_and_rejects_out_of_range_keys() {
    let mut state = unlocked_home();
    assert_eq!(drive(&mut state, Input::ToggleSetting(2)), Err(Error::InvalidTransition));
    drive(&mut state, Input::OpenSettings).unwrap();
    let Outcome::SettingToggled(receipt) = drive(&mut state, Input::ToggleSetting(7)).unwrap() else {
        panic!("last key must be toggleable")
    };
    assert_eq!(receipt.settings, [1, 0, 0, 0, 0, 0, 0, 1]);
    drive(&mut state, Input::ToggleSetting(7)).unwrap();
    assert_eq!(state.settings(), S553_DEFAULT_SETTINGS);
    assert_eq!(
        drive(&mut state, Input::ToggleSetting(S553_SETTINGS_CAPACITY as u8)),
        Err(Error::SettingKeyOutOfRange)
    );
    assert_eq!(drive(&mut state, Input::ToggleSetting(u8::MAX)), Err(Error::SettingKeyOutOfRange));
    assert_eq!(state.settings(), S553_DEFAULT_SETTINGS);
    assert!(state.settings().iter().all(|flag| *flag <= 1));
}

#[test]
fn status_bar_rejects_out_of_range_battery_and_signal() {
    let mut state = G8lS553SystemUiState::new();
    let Outcome::StatusUpdated(receipt) = drive(&mut state, Input::BatteryReport(100)).unwrap() else {
        panic!("battery 100 must be accepted")
    };
    assert_eq!(receipt.status_bar.battery_percent, 100);
    assert_eq!(receipt.to_scene, Scene::Lock);
    assert_eq!(drive(&mut state, Input::BatteryReport(101)), Err(Error::BatteryOutOfRange));
    let Outcome::StatusUpdated(receipt) = drive(&mut state, Input::SignalReport(5)).unwrap() else {
        panic!("signal 5 must be accepted")
    };
    assert_eq!(receipt.status_bar.signal_bars, 5);
    assert_eq!(receipt.status_bar.battery_percent, 100);
    assert_eq!(drive(&mut state, Input::SignalReport(6)), Err(Error::SignalOutOfRange));
    assert_eq!(drive(&mut state, Input::SignalReport(u8::MAX)), Err(Error::SignalOutOfRange));
    assert_eq!(state.status_bar().signal_bars, 5);
    assert_eq!(state.status_bar().battery_percent, 100);
    assert_eq!(state.accepted_events(), 2);
}

#[test]
fn clock_derives_hh_mm_from_ticks_and_wraps_at_midnight() {
    assert_eq!(s553_clock_from_ticks(0), (0, 0));
    assert_eq!(s553_clock_from_ticks(S553_TICKS_PER_MINUTE - 1), (0, 0));
    assert_eq!(s553_clock_from_ticks(S553_TICKS_PER_MINUTE), (0, 1));
    assert_eq!(s553_clock_from_ticks(S553_TICKS_PER_MINUTE * 61), (1, 1));
    assert_eq!(s553_clock_from_ticks(S553_TICKS_PER_MINUTE * 1_439), (23, 59));
    assert_eq!(s553_clock_from_ticks(S553_TICKS_PER_MINUTE * 1_440), (0, 0));
    assert_eq!(s553_clock_from_ticks(u64::MAX), (0, 18));
    assert_eq!(s553_clock_text(23, 59), *b"23:59");
    assert_eq!(s553_clock_text(7, 5), *b"07:05");

    let mut state = G8lS553SystemUiState::new();
    let Outcome::StatusUpdated(receipt) =
        drive(&mut state, Input::Tick(S553_TICKS_PER_MINUTE * (13 * 60 + 37))).unwrap()
    else {
        panic!("tick must update status")
    };
    assert_eq!(receipt.status_bar.clock_hour, 13);
    assert_eq!(receipt.status_bar.clock_minute, 37);
    assert_eq!(receipt.status_bar.clock_text, *b"13:37");
    assert_eq!(receipt.status_bar.tick_count, S553_TICKS_PER_MINUTE * 817);
    let Outcome::StatusUpdated(receipt) = drive(&mut state, Input::Tick(u64::MAX)).unwrap() else {
        panic!("max tick must update status")
    };
    assert_eq!(receipt.status_bar.clock_text, *b"00:18");
}

#[test]
fn tick_regression_and_lockout_arithmetic_overflow_fail_closed() {
    let mut state = G8lS553SystemUiState::new();
    drive(&mut state, Input::Tick(500)).unwrap();
    assert_eq!(drive(&mut state, Input::Tick(499)), Err(Error::TickRegression));
    assert!(matches!(drive(&mut state, Input::Tick(500)), Ok(Outcome::StatusUpdated(_))));
    drive(&mut state, Input::Tick(u64::MAX - 1)).unwrap();
    for _ in 0..S553_MAX_PIN_ATTEMPTS {
        drive(&mut state, Input::PinEntry([0, 0, 0, 0])).unwrap();
    }
    assert_eq!(state.pin_failed_attempts(), S553_MAX_PIN_ATTEMPTS);
    assert_eq!(drive(&mut state, Input::PinEntry([0, 0, 0, 0])), Err(Error::TickOverflow));
    assert_eq!(state.pin_failed_attempts(), S553_MAX_PIN_ATTEMPTS);
    assert_eq!(state.lockout_count(), 0);
    assert!(!state.locked_out());
    assert_eq!(state.accepted_events(), 3 + u64::from(S553_MAX_PIN_ATTEMPTS));
}

#[test]
fn lockout_counter_saturation_fails_closed() {
    let mut state = G8lS553SystemUiState::new();
    let mut tick = 0u64;
    for round in 1..=u8::MAX {
        for _ in 0..=S553_MAX_PIN_ATTEMPTS {
            drive(&mut state, Input::PinEntry([5, 5, 5, 5])).unwrap();
        }
        assert_eq!(state.lockout_count(), round);
        tick += S553_LOCKOUT_TICKS;
        drive(&mut state, Input::Tick(tick)).unwrap();
        assert!(!state.locked_out());
    }
    for _ in 0..S553_MAX_PIN_ATTEMPTS {
        drive(&mut state, Input::PinEntry([5, 5, 5, 5])).unwrap();
    }
    assert_eq!(
        drive(&mut state, Input::PinEntry([5, 5, 5, 5])),
        Err(Error::LockoutCounterOverflow)
    );
    assert_eq!(state.lockout_count(), u8::MAX);
    assert!(!state.locked_out());
    assert!(matches!(
        drive(&mut state, Input::PinEntry(S553_DEFAULT_PIN)),
        Ok(Outcome::Transitioned(_))
    ));
}

#[test]
fn event_ids_must_be_contiguous() {
    let mut state = G8lS553SystemUiState::new();
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(0, Input::Tick(1))),
        Err(Error::EventOrder)
    );
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(2, Input::Tick(1))),
        Err(Error::EventOrder)
    );
    service_s553_model_scene_flow(&mut state, event(1, Input::Tick(1))).unwrap();
    service_s553_model_scene_flow(&mut state, event(2, Input::Tick(2))).unwrap();
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(1, Input::Tick(1))),
        Err(Error::EventOrder)
    );
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(4, Input::Tick(4))),
        Err(Error::EventOrder)
    );
    assert_eq!(
        service_s553_model_scene_flow(&mut state, event(u64::MAX, Input::Tick(4))),
        Err(Error::EventOrder)
    );
    assert_eq!(state.accepted_events(), 2);
    assert_eq!(state.status_bar().tick_count, 2);
}

#[test]
fn pin_digits_out_of_range_are_rejected() {
    let mut state = G8lS553SystemUiState::new();
    for pin in [[10, 0, 0, 0], [0, 0, 0, 10], [1, 2, 3, 255]] {
        assert_eq!(drive(&mut state, Input::PinEntry(pin)), Err(Error::PinDigitOutOfRange));
    }
    assert_eq!(state.pin_failed_attempts(), 0);
    assert_eq!(state.accepted_events(), 0);
    assert_eq!(
        G8lS553SystemUiState::with_pin([0, 0, 1, 10]).err(),
        Some(Error::PinDigitOutOfRange)
    );
    let mut custom = G8lS553SystemUiState::with_pin([0, 9, 0, 9]).unwrap();
    assert!(matches!(
        drive(&mut custom, Input::PinEntry(S553_DEFAULT_PIN)),
        Ok(Outcome::UnlockRejected(_))
    ));
    assert!(matches!(
        drive(&mut custom, Input::PinEntry([0, 9, 0, 9])),
        Ok(Outcome::Transitioned(_))
    ));
}

#[test]
fn constant_time_pin_compare_examines_every_digit() {
    assert!(s553_pin_matches_constant_time([1, 2, 3, 4], [1, 2, 3, 4]));
    assert!(s553_pin_matches_constant_time([0, 0, 0, 0], [0, 0, 0, 0]));
    for position in 0..S553_PIN_DIGITS {
        let mut entered = S553_DEFAULT_PIN;
        entered[position] ^= 0b1000;
        assert!(!s553_pin_matches_constant_time(entered, S553_DEFAULT_PIN));
    }
    assert!(!s553_pin_matches_constant_time([4, 3, 2, 1], S553_DEFAULT_PIN));
    assert!(s553_pin_digits_are_valid([9, 9, 9, 9]));
    assert!(!s553_pin_digits_are_valid([9, 9, 9, 10]));
    let compare = SOURCE
        .split("pub fn s553_pin_matches_constant_time")
        .nth(1)
        .unwrap()
        .split("pub fn s553_pin_digits_are_valid")
        .next()
        .unwrap();
    assert!(compare.contains("difference |= entered[index] ^ expected[index]"));
    assert!(!compare.contains("return false"));
    assert!(!compare.contains("break"));
}

#[test]
fn transition_table_is_explicit_and_unambiguous() {
    assert_eq!(S553_TRANSITION_TABLE.len(), 11);
    let mut pairs = BTreeSet::new();
    for entry in S553_TRANSITION_TABLE {
        assert!(pairs.insert((entry.from.index(), entry.kind as u8)));
        assert!(!matches!(
            entry.kind,
            G8lS553EventKind::Tick | G8lS553EventKind::BatteryReport | G8lS553EventKind::SignalReport
        ));
        assert_eq!(s553_lookup_transition(entry.from, entry.kind), Some(entry.action));
    }
    assert!(!S553_TRANSITION_TABLE
        .iter()
        .any(|entry| entry.from == Scene::Lock
            && entry.action == G8lS553TransitionAction::Push(Scene::Settings)));
    assert_eq!(
        s553_lookup_transition(Scene::Home, G8lS553EventKind::PinEntry),
        None
    );
    assert_eq!(
        s553_lookup_transition(Scene::App, G8lS553EventKind::ToggleSetting),
        None
    );
    assert_eq!(
        s553_lookup_transition(Scene::Home, G8lS553EventKind::Back),
        Some(G8lS553TransitionAction::Lock)
    );
    assert_eq!(Scene::Lock.index(), 0);
    assert_eq!(Scene::App.index(), 3);
}

#[test]
fn invalid_transition_leaves_state_untouched() {
    let mut state = unlocked_home();
    drive(&mut state, Input::BatteryReport(42)).unwrap();
    let receipt = receipt_of(drive(&mut state, Input::OpenSettings).unwrap());
    assert_eq!(state.last_receipt(), Some(receipt));
    let scene = state.current_scene();
    let depth = state.stack_depth();
    let settings = state.settings();
    let status = state.status_bar();
    let accepted = state.accepted_events();
    for input in [
        Input::UnlockGesture,
        Input::PinEntry(S553_DEFAULT_PIN),
        Input::OpenSettings,
        Input::ToggleSetting(8),
        Input::BatteryReport(200),
        Input::SignalReport(9),
    ] {
        assert!(drive(&mut state, input).is_err());
    }
    assert_eq!(state.current_scene(), scene);
    assert_eq!(state.stack_depth(), depth);
    assert_eq!(state.settings(), settings);
    assert_eq!(state.status_bar(), status);
    assert_eq!(state.last_receipt(), Some(receipt));
    assert_eq!(state.accepted_events(), accepted);
    assert_eq!(scene, Scene::Settings);
    assert_eq!(status.battery_percent, 42);
}

  {
    id: "g8l-s553-r1-system-ui-lock-status-settings-scene-flow-model",
    date: "2026-08-30",
    sequence: 553,
    status: "passed",
    umbrella_status: "partial",
    title: "S553 · R1 ekran: kilit/durum/ayar ekranları system UI akış modeli",
    summary:
      "S553 kaynak/host model kapısı PASS'tir: kernel/src/ui/scene.rs retained scene soyutlamasının üzerinde Lock, Home (durum), Settings ve App (placeholder) sahnelerinden oluşan kontrollü system-UI akışı, 11 satırlık açık geçiş tablosu, sabit-zamanlı 4 haneli PIN karşılaştırması, 5 deneme sonrası kilitlenme sayacı, derinliği en fazla 4 olan sahne yığını, 8 slotluk u8 bayrak ayar deposu ve pil yüzdesi / sinyal çubuğu (0..5) / tick sayısından türetilen HH:MM saat içeren durum çubuğu olarak modellendi. Her kabul edilen olay sıra numaralı bir SceneReceipt üretir; geçersiz geçişler, aralık dışı değerler, tick gerilemesi, aritmetik taşma, yığın taşması, sıra dışı olay id'si ve yayın sonrası sapma fail-closed reddedilir ve durumu değiştirmez. Focused 24/24 PASS'tir. S540 ve S543 fiziksel RED değişmez kalır; hardware=none, physical observation=0, RUNBOOK_EXECUTED_IN_S553=NO, Boot-to-UI=false ve R1 acceptance=false'dur. S554 host-only modem AT komut taşıma çerçeveleme modeli kapısıdır.",
    evidence: [
      "S553, kernel/src/ui/scene.rs retained Scene/Layer soyutlamasının üzerine oturacak kontrollü system-UI akışını Lock, Home (durum), Settings ve App (placeholder) sahneleriyle salt kaynak/host modeli olarak tanımlar; hiçbir panel, dokunmatik denetleyici, framebuffer grant, modem, board veya UART bu kapıda mevcut değildir.",
      "Geçiş tablosu S553_TRANSITION_TABLE 11 açık satırdan oluşur: Lock→Home (gesture yalnız PIN_REQUIRED=0 iken, PinEntry sabit-zamanlı eşleşmede), Home→Settings/App push, Home Back→Lock, Settings ToggleSetting stay, Settings/App Back pop, Settings→App ve App→Settings push; tabloda olmayan her (sahne, olay) çifti InvalidTransition ile reddedilir.",
      "Lock sahnesinden OpenSettings açık bir guard satırıyla SettingsFromLockForbidden döner; Lock'tan OpenApp, Back ve ToggleSetting InvalidTransition'dır.",
      "PIN karşılaştırması s553_pin_matches_constant_time ile tüm 4 haneyi XOR-OR biriktirerek erken dönüşsüz yapılır; 9'dan büyük hane PinDigitOutOfRange ile reddedilir.",
      "S553_MAX_PIN_ATTEMPTS=5'tir; altıncı ardışık hatalı PIN LockedOut sonucu üretir, lockout_count checked u8 ile artar, deneme sayacı sıfırlanır ve lockout_release_tick=tick+3000 (30 s, 100 Hz) checked u64 ile hesaplanır; kilit süresince her unlock olayı Err(LockedOut) döner ve serbest bırakma tick'ine ulaşan Tick kilidi kaldırır.",
      "Sahne yığını S553_SCENE_STACK_MAX_DEPTH=4 ile sınırlıdır; dördüncü push kabul edilir, beşinci push SceneStackOverflow ile reddedilir ve yığın değişmez.",
      "Ayar deposu 8 slotluk u8 bayraktır (anahtar 0 = PIN_REQUIRED, varsayılan 1); ToggleSetting yalnız Settings sahnesinde, anahtar<8 ve değer<=1 iken kabul edilir, 8 ve 255 anahtarları SettingKeyOutOfRange döner.",
      "Durum çubuğu pil 0..=100, sinyal 0..=5 ve tick sayısından türetilen HH:MM saati (minute_of_day = tick/6000 % 1440) beş baytlık ASCII clock_text ile taşır; 101 pil, 6/255 sinyal ve tick gerilemesi fail-closed reddedilir; u64::MAX tick 00:18 olarak sarar.",
      "Her kabul edilen olay sequence=553, predecessor=552, artan transition_sequence, olay id/kind, from/to sahne, tam yığın, durum çubuğu, ayar anlık görüntüsü, deneme/lockout sayaçları, hardware_present=false, physical_observations=0 ve runbook_executed=false alanlı bir G8lS553SceneReceipt üretir.",
      "service_s553_model_scene_flow sonraki anlık görüntüyü yerel olarak hesaplar ve yalnız başarıda commit eder; olay id'leri bitişik olmak zorundadır (0, atlanmış, bayat ve u64::MAX id EventOrder), son kabul edilen olayın birebir tekrarı Retained ile aynı receipt'i döndürür, aynı id altında farklı payload PublishedEventDivergence'tır.",
      "On yedi hata kodu 1..=17 aralığında benzersiz ve sıfırdan farklıdır; TickOverflow (u64::MAX-1 tick'te altıncı hatalı PIN) ve LockoutCounterOverflow (255 lockout sonrası 256.) focused testte doğrulanmıştır.",
      "Focused target 1 grup / 24 passed / 0 failed / 0 ignored / 0 filtered verdi; 6 sözleşme testi ve 18 alan testi (mutlu yol, sınır değerleri, bozuk girdi, taşma, sıralama) içerir.",
      "Implementation 23913 B / cedaf20d38f88ff1914ff08e858b0240e57c279495ea0a9e86b40aef55cc1745; focused test 24302 B / 60edc05d1b322d449748d9761fd6a635e2edab6484672b8bbc5fe5b4f8f09f29 SHA-256'dır.",
      "Proof 6202 B'dır.",
      "Modül hiçbir boot, IRQ, scheduler veya sürücü yoluna bağlanmamıştır; unsafe, asm!, write_volatile, crate::uart, crate::arch, #[no_mangle] ve spin:: yüzeyi içermez.",
      "S540 immutable raw 20525 B ve S543 immutable raw 20509 B fiziksel RED kararlarıyla byte-exact korunur; automatic promotion=false ve rerun=false'dur.",
      "S553 sırasında candidate freeze, SD write/read-back/eject, UART open/capture, power transition, fiziksel koşu veya yeni immutable raw üretimi yapılmadı.",
      "RUNBOOK_EXECUTED_IN_S553=NO; supported-profile runtime observations=0, physical observations=0, hardware present=false, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.",
      "S554 yalnız host üzerinde modem AT komut taşıma çerçeveleme modelini tanımlayacaktır; aygıt, modem veya fiziksel koşu yetkisi değildir.",
    ],
    commands: [
      "CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s553_r1_system_ui_lock_status_settings_scene_flow_model -- --test-threads=1",
    ],
    terminalSessions: [
      {
        id: "s553-focused",
        title: "S553 system UI scene flow model focused acceptance",
        commandLines: [
          "CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s553_r1_system_ui_lock_status_settings_scene_flow_model -- --test-threads=1",
        ],
        outputLines: [
          "test result: ok. 24 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s",
          "S553 focused=1 group / 24 passed / 0 failed",
          "hardware=none physical=0 runbook=NO",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
    ],
    terminalSessionsNote:
      "S553 kaynak/host model PASS'tir; supported-profile runtime veya fiziksel PASS değildir. S540 ve S543 RED raw ve kararları değişmez.",
    limitations: [
      "S553 yalnız kaynak/host system-UI akış modelidir; hiçbir donanım/panel/modem/board gözlemi yoktur ve modül hiçbir üretim çağrı noktasına bağlanmamıştır.",
      "Sahne akışı kernel/src/ui/scene.rs Layer/Scene compositing'ine henüz bağlanmamıştır; gerçek framebuffer grant, dokunma girişi veya vsync olayı bu kapıda yoktur.",
      "Varsayılan PIN bir model fikstürüdür; gerçek kimlik doğrulama, güvenli depolama veya kalıcı ayar saklama modellenmemiştir.",
      "S540 ve S543 fiziksel RED immutable kalır; otomatik yükseltme veya yeniden koşu yapılmaz.",
      "Boot-to-UI fiziksel olarak gözlenmedi; R1 acceptance false kalır ve RUNBOOK_EXECUTED_IN_S553=NO'dur.",
      "S554 host-only modem AT komut taşıma çerçeveleme modeli tamamlanmadan R1 3. aşama (modem/ses) için kaynak modeli yoktur; yeni SD/UART/power koşusu ayrı kapı, fresh target revalidation, açık operatör yetkisi ve yeni immutable raw ister.",
    ],
  },