S547 · R1 ekran: VideoCore mailbox framebuffer tahsis sözleşmesi

//! S547 models the VideoCore property-mailbox framebuffer allocation
//! transaction that a Raspberry Pi 5 HDMI first-pixel path would issue.
//!
//! The model covers the exact word layout of a property buffer (total byte
//! size, request code `0`, seven tags, end tag `0`, 16-byte padding), the tag
//! identifiers `0x00048003` set physical size, `0x00048004` set virtual size,
//! `0x00048005` set depth (32), `0x00048006` set pixel order (BGR),
//! `0x00040001` allocate (4096-byte alignment), `0x00040008` get pitch and
//! `0x00048009` set virtual offset, the firmware response code
//! `0x80000000` / `0x80000001`, the per-tag response bit, the bus-to-ARM
//! address conversion (`& 0x3FFF_FFFF`), the `pitch >= width * 4` and
//! `size >= pitch * height` checks, and a `G8lS547FramebufferAllocationReceipt`
//! that a later gate may turn into a `ui::framebuffer::FramebufferCap`.
//!
//! Two display profiles are tabled: the 720x1280 portrait Touch Display 2
//! target (default) and a 1920x1080 HDMI lab profile.
//!
//! This gate does NOT claim any hardware: no mailbox MMIO, no VideoCore
//! response, no panel, no HDMI sink and no board observation exist.  The
//! firmware reply is a host-side model that the focused test drives.  The
//! module is not wired into any boot, IRQ, scheduler or driver path and does
//! not modify `driver::mailbox`; it only mirrors its `PropertyBuffer` naming
//! (`data: [u32; 36]`, property channel 8).  It performs no device operation,
//! emits no UART text and cannot promote the immutable S540/S543 physical RED.
//!
//! Predecessor: S546 (third physical run, verdict pending separately).
//! Next gate: S548 (test-pattern framebuffer capability binding).

pub const S547_SEQUENCE: usize = 547;
pub const S547_EXPECTED_PREDECESSOR: usize = 546;
pub const S547_R1_STAGE: u8 = 2;
pub const S547_R1_RANGE_FIRST: usize = 536;
pub const S547_R1_RANGE_LAST: usize = 568;
pub const S547_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS: usize = 0;
pub const S547_PHYSICAL_OBSERVATIONS: usize = 0;
pub const S547_PHYSICAL_OR_DEVICE_OPERATIONS: usize = 0;
pub const S547_SD_WRITES: usize = 0;
pub const S547_UART_OPENS: usize = 0;
pub const S547_POWER_TRANSITIONS: usize = 0;
pub const S547_NEW_IMMUTABLE_RAW_CAPTURES: usize = 0;
pub const S547_S540_PHYSICAL_VERDICT_RETAINED_RED: bool = true;
pub const S547_S543_PHYSICAL_VERDICT_RETAINED_RED: bool = true;
pub const S547_AUTOMATIC_PROMOTION: bool = false;
pub const S547_BOOT_TO_UI_PHYSICALLY_OBSERVED: bool = false;
pub const S547_HARDWARE_PRESENT: bool = false;
pub const S547_R1_ACCEPTANCE_COMPLETE: bool = false;
pub const RUNBOOK_EXECUTED_IN_S547: bool = false;

/// Property channel of the ARM-to-VideoCore mailbox (`driver::mailbox::CHANNEL`).
pub const S547_PROPERTY_CHANNEL: u32 = 8;
/// Word count of the property buffer; equals `driver::mailbox::PropertyBuffer::data`.
pub const S547_PROPERTY_BUFFER_WORDS: usize = 36;
/// Byte size of the property buffer (word 0); a multiple of 16.
pub const S547_PROPERTY_BUFFER_BYTES: u32 = (S547_PROPERTY_BUFFER_WORDS * 4) as u32;
pub const S547_PROPERTY_BUFFER_ALIGNMENT: u32 = 16;
pub const S547_REQUEST_CODE: u32 = 0x0000_0000;
pub const S547_RESPONSE_SUCCESS: u32 = 0x8000_0000;
pub const S547_RESPONSE_ERROR_PARSING: u32 = 0x8000_0001;
pub const S547_TAG_RESPONSE_BIT: u32 = 0x8000_0000;
pub const S547_END_TAG: u32 = 0x0000_0000;
pub const S547_TAG_SET_PHYSICAL_SIZE: u32 = 0x0004_8003;
pub const S547_TAG_SET_VIRTUAL_SIZE: u32 = 0x0004_8004;
pub const S547_TAG_SET_DEPTH: u32 = 0x0004_8005;
pub const S547_TAG_SET_PIXEL_ORDER: u32 = 0x0004_8006;
pub const S547_TAG_ALLOCATE_BUFFER: u32 = 0x0004_0001;
pub const S547_TAG_GET_PITCH: u32 = 0x0004_0008;
pub const S547_TAG_SET_VIRTUAL_OFFSET: u32 = 0x0004_8009;
pub const S547_DEPTH_BITS: u32 = 32;
pub const S547_BYTES_PER_PIXEL: u32 = S547_DEPTH_BITS / 8;
pub const S547_PIXEL_ORDER_BGR: u32 = 0;
pub const S547_PIXEL_ORDER_RGB: u32 = 1;
pub const S547_ALLOCATE_ALIGNMENT: u32 = 4096;
pub const S547_BUS_TO_ARM_MASK: u32 = 0x3FFF_FFFF;
pub const S547_VIRTUAL_OFFSET_X: u32 = 0;
pub const S547_VIRTUAL_OFFSET_Y: u32 = 0;
pub const S547_TAG_COUNT: usize = 7;
pub const S547_PORTRAIT_WIDTH: u32 = 720;
pub const S547_PORTRAIT_HEIGHT: u32 = 1280;
pub const S547_HDMI_LAB_WIDTH: u32 = 1920;
pub const S547_HDMI_LAB_HEIGHT: u32 = 1080;

/// Word indices inside the property buffer.
pub const S547_WORD_BUFFER_SIZE: usize = 0;
pub const S547_WORD_REQUEST_CODE: usize = 1;
pub const S547_WORD_PHYSICAL_SIZE_TAG: usize = 2;
pub const S547_WORD_VIRTUAL_SIZE_TAG: usize = 7;
pub const S547_WORD_DEPTH_TAG: usize = 12;
pub const S547_WORD_PIXEL_ORDER_TAG: usize = 16;
pub const S547_WORD_ALLOCATE_TAG: usize = 20;
pub const S547_WORD_PITCH_TAG: usize = 25;
pub const S547_WORD_VIRTUAL_OFFSET_TAG: usize = 29;
pub const S547_WORD_END_TAG: usize = 34;
pub const S547_WORD_PADDING: usize = 35;

/// One tag of the transaction: identifier, value-buffer byte size and the
/// word index of its identifier inside the buffer.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS547TagDescriptor {
    pub tag: u32,
    pub value_bytes: u32,
    pub word_index: usize,
}

impl G8lS547TagDescriptor {
    pub const fn value_words(self) -> usize {
        (self.value_bytes / 4) as usize
    }

    pub const fn first_value_word(self) -> usize {
        self.word_index + 3
    }

    pub const fn end_word(self) -> usize {
        self.first_value_word() + self.value_words()
    }
}

pub const S547_TAG_TABLE: [G8lS547TagDescriptor; S547_TAG_COUNT] = [
    G8lS547TagDescriptor {
        tag: S547_TAG_SET_PHYSICAL_SIZE,
        value_bytes: 8,
        word_index: S547_WORD_PHYSICAL_SIZE_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_SET_VIRTUAL_SIZE,
        value_bytes: 8,
        word_index: S547_WORD_VIRTUAL_SIZE_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_SET_DEPTH,
        value_bytes: 4,
        word_index: S547_WORD_DEPTH_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_SET_PIXEL_ORDER,
        value_bytes: 4,
        word_index: S547_WORD_PIXEL_ORDER_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_ALLOCATE_BUFFER,
        value_bytes: 8,
        word_index: S547_WORD_ALLOCATE_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_GET_PITCH,
        value_bytes: 4,
        word_index: S547_WORD_PITCH_TAG,
    },
    G8lS547TagDescriptor {
        tag: S547_TAG_SET_VIRTUAL_OFFSET,
        value_bytes: 8,
        word_index: S547_WORD_VIRTUAL_OFFSET_TAG,
    },
];

/// Display profiles tabled for the R1 first-pixel path.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS547DisplayProfile {
    /// 5"/7" Touch Display 2 in portrait orientation (default target).
    TouchDisplay2Portrait,
    /// 1920x1080 HDMI lab monitor profile.
    HdmiLab1080p,
}

impl G8lS547DisplayProfile {
    pub const fn width(self) -> u32 {
        match self {
            Self::TouchDisplay2Portrait => S547_PORTRAIT_WIDTH,
            Self::HdmiLab1080p => S547_HDMI_LAB_WIDTH,
        }
    }

    pub const fn height(self) -> u32 {
        match self {
            Self::TouchDisplay2Portrait => S547_PORTRAIT_HEIGHT,
            Self::HdmiLab1080p => S547_HDMI_LAB_HEIGHT,
        }
    }

    pub const fn profile_code(self) -> u8 {
        match self {
            Self::TouchDisplay2Portrait => 1,
            Self::HdmiLab1080p => 2,
        }
    }
}

impl Default for G8lS547DisplayProfile {
    fn default() -> Self {
        Self::TouchDisplay2Portrait
    }
}

/// Host-side mirror of `driver::mailbox::PropertyBuffer` (`data: [u32; 36]`).
/// Alignment is modelled by the byte-size word, not by a memory placement.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS547PropertyBufferWords {
    pub data: [u32; S547_PROPERTY_BUFFER_WORDS],
}

impl G8lS547PropertyBufferWords {
    pub const fn new() -> Self {
        Self {
            data: [0; S547_PROPERTY_BUFFER_WORDS],
        }
    }
}

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

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS547FramebufferAllocationReceipt {
    pub sequence: usize,
    pub predecessor_sequence: usize,
    pub r1_stage: u8,
    pub profile: G8lS547DisplayProfile,
    pub width: u32,
    pub height: u32,
    pub virtual_width: u32,
    pub virtual_height: u32,
    pub depth_bits: u32,
    pub pixel_order: u32,
    pub virtual_offset_x: u32,
    pub virtual_offset_y: u32,
    pub bus_address: u32,
    /// `bus_address & 0x3FFF_FFFF`; seeds `FramebufferCap::phys_addr`.
    pub arm_physical_address: u32,
    pub buffer_size_bytes: u32,
    /// Bytes per row; seeds `FramebufferCap::stride`.
    pub pitch: u32,
    pub minimum_pitch: u32,
    pub minimum_size_bytes: u32,
    pub allocate_alignment: u32,
    pub property_buffer_bytes: u32,
    pub property_channel: u32,
    pub response_code: u32,
    pub tag_count: usize,
    pub hardware_present: bool,
    pub mmio_performed: bool,
    pub s540_physical_verdict_retained_red: bool,
    pub s543_physical_verdict_retained_red: bool,
    pub automatic_promotion: bool,
    pub supported_profile_runtime_observations: usize,
    pub physical_observations: usize,
    pub boot_to_ui_physically_observed: bool,
    pub r1_acceptance_complete: bool,
    pub runbook_executed: bool,
}

#[derive(Debug)]
pub struct G8lS547FramebufferAllocationState {
    receipt: Option<G8lS547FramebufferAllocationReceipt>,
    request: Option<G8lS547PropertyBufferWords>,
    response: Option<G8lS547PropertyBufferWords>,
}

impl G8lS547FramebufferAllocationState {
    pub const fn new() -> Self {
        Self {
            receipt: None,
            request: None,
            response: None,
        }
    }

    pub const fn receipt(&self) -> Option<G8lS547FramebufferAllocationReceipt> {
        self.receipt
    }

    pub const fn published_request(&self) -> Option<G8lS547PropertyBufferWords> {
        self.request
    }

    pub const fn published_response(&self) -> Option<G8lS547PropertyBufferWords> {
        self.response
    }
}

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

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS547FramebufferAllocationOutcome {
    Allocated(G8lS547FramebufferAllocationReceipt),
    Retained(G8lS547FramebufferAllocationReceipt),
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS547FramebufferAllocationError {
    BufferSizeWordDrift,
    BufferSizeNotAligned,
    RequestCodeNotZero,
    ResponseErrorParsing,
    ResponseCodeInvalid,
    TagIdentifierDrift,
    TagValueSizeDrift,
    TagResponseBitMissing,
    TagResponseLengthDrift,
    EndTagMissing,
    PaddingNotZero,
    PhysicalSizeDrift,
    VirtualSizeDrift,
    DepthDrift,
    PixelOrderDrift,
    VirtualOffsetDrift,
    BusAddressZero,
    ArmAddressMisaligned,
    BufferSizeZero,
    PitchBelowMinimum,
    PitchNotWordAligned,
    PitchHeightOverflow,
    BufferSizeBelowMinimum,
    AddressRangeOverflow,
    PublishedStateDrift,
}

impl G8lS547FramebufferAllocationError {
    pub const fn diagnostic_code(self) -> u64 {
        match self {
            Self::BufferSizeWordDrift => 1,
            Self::BufferSizeNotAligned => 2,
            Self::RequestCodeNotZero => 3,
            Self::ResponseErrorParsing => 4,
            Self::ResponseCodeInvalid => 5,
            Self::TagIdentifierDrift => 6,
            Self::TagValueSizeDrift => 7,
            Self::TagResponseBitMissing => 8,
            Self::TagResponseLengthDrift => 9,
            Self::EndTagMissing => 10,
            Self::PaddingNotZero => 11,
            Self::PhysicalSizeDrift => 12,
            Self::VirtualSizeDrift => 13,
            Self::DepthDrift => 14,
            Self::PixelOrderDrift => 15,
            Self::VirtualOffsetDrift => 16,
            Self::BusAddressZero => 17,
            Self::ArmAddressMisaligned => 18,
            Self::BufferSizeZero => 19,
            Self::PitchBelowMinimum => 20,
            Self::PitchNotWordAligned => 21,
            Self::PitchHeightOverflow => 22,
            Self::BufferSizeBelowMinimum => 23,
            Self::AddressRangeOverflow => 24,
            Self::PublishedStateDrift => 25,
        }
    }
}

/// Converts a VideoCore bus address into an ARM physical address.
pub const fn s547_bus_to_arm_address(bus_address: u32) -> u32 {
    bus_address & S547_BUS_TO_ARM_MASK
}

/// Minimum pitch for a profile: `width * 4` with a checked multiply.
pub const fn s547_minimum_pitch(width: u32) -> Option<u32> {
    width.checked_mul(S547_BYTES_PER_PIXEL)
}

/// Encodes the request words for a profile.  Every tag carries request code
/// `0` in its response-length word; the allocate value carries the alignment.
pub fn encode_s547_framebuffer_request(
    profile: G8lS547DisplayProfile,
) -> G8lS547PropertyBufferWords {
    let mut words = G8lS547PropertyBufferWords::new();
    let data = &mut words.data;
    data[S547_WORD_BUFFER_SIZE] = S547_PROPERTY_BUFFER_BYTES;
    data[S547_WORD_REQUEST_CODE] = S547_REQUEST_CODE;
    for descriptor in S547_TAG_TABLE {
        data[descriptor.word_index] = descriptor.tag;
        data[descriptor.word_index + 1] = descriptor.value_bytes;
        data[descriptor.word_index + 2] = S547_REQUEST_CODE;
    }
    let physical = S547_TAG_TABLE[0].first_value_word();
    data[physical] = profile.width();
    data[physical + 1] = profile.height();
    let virtual_size = S547_TAG_TABLE[1].first_value_word();
    data[virtual_size] = profile.width();
    data[virtual_size + 1] = profile.height();
    data[S547_TAG_TABLE[2].first_value_word()] = S547_DEPTH_BITS;
    data[S547_TAG_TABLE[3].first_value_word()] = S547_PIXEL_ORDER_BGR;
    let allocate = S547_TAG_TABLE[4].first_value_word();
    data[allocate] = S547_ALLOCATE_ALIGNMENT;
    data[allocate + 1] = 0;
    data[S547_TAG_TABLE[5].first_value_word()] = 0;
    let offset = S547_TAG_TABLE[6].first_value_word();
    data[offset] = S547_VIRTUAL_OFFSET_X;
    data[offset + 1] = S547_VIRTUAL_OFFSET_Y;
    data[S547_WORD_END_TAG] = S547_END_TAG;
    data[S547_WORD_PADDING] = 0;
    words
}

/// Host-side model of a compliant firmware reply to an encoded request.
/// It is not a VideoCore response; the focused test perturbs it to exercise
/// the fail-closed decoder.
pub fn model_s547_firmware_response(
    request: &G8lS547PropertyBufferWords,
    bus_address: u32,
    buffer_size_bytes: u32,
    pitch: u32,
) -> G8lS547PropertyBufferWords {
    let mut words = *request;
    let data = &mut words.data;
    data[S547_WORD_REQUEST_CODE] = S547_RESPONSE_SUCCESS;
    for descriptor in S547_TAG_TABLE {
        data[descriptor.word_index + 2] = S547_TAG_RESPONSE_BIT | descriptor.value_bytes;
    }
    let allocate = S547_TAG_TABLE[4].first_value_word();
    data[allocate] = bus_address;
    data[allocate + 1] = buffer_size_bytes;
    data[S547_TAG_TABLE[5].first_value_word()] = pitch;
    words
}

fn check_tag_frames(
    request: &G8lS547PropertyBufferWords,
    response: &G8lS547PropertyBufferWords,
) -> Result<(), G8lS547FramebufferAllocationError> {
    use G8lS547FramebufferAllocationError as E;
    let mut expected_next = S547_WORD_PHYSICAL_SIZE_TAG;
    for descriptor in S547_TAG_TABLE {
        if descriptor.word_index != expected_next {
            return Err(E::TagIdentifierDrift);
        }
        let index = descriptor.word_index;
        if request.data[index] != descriptor.tag || response.data[index] != descriptor.tag {
            return Err(E::TagIdentifierDrift);
        }
        if request.data[index + 1] != descriptor.value_bytes
            || response.data[index + 1] != descriptor.value_bytes
        {
            return Err(E::TagValueSizeDrift);
        }
        let status = response.data[index + 2];
        if status & S547_TAG_RESPONSE_BIT == 0 {
            return Err(E::TagResponseBitMissing);
        }
        if status & !S547_TAG_RESPONSE_BIT != descriptor.value_bytes {
            return Err(E::TagResponseLengthDrift);
        }
        expected_next = descriptor.end_word();
    }
    if expected_next != S547_WORD_END_TAG {
        return Err(E::EndTagMissing);
    }
    Ok(())
}

/// Decodes a firmware response against the request it answers.  Every
/// malformed word, echo drift, overflow or under-sized allocation fails closed.
pub fn decode_s547_framebuffer_response(
    profile: G8lS547DisplayProfile,
    request: &G8lS547PropertyBufferWords,
    response: &G8lS547PropertyBufferWords,
) -> Result<G8lS547FramebufferAllocationReceipt, G8lS547FramebufferAllocationError> {
    use G8lS547FramebufferAllocationError as E;
    let size_word = response.data[S547_WORD_BUFFER_SIZE];
    if size_word != S547_PROPERTY_BUFFER_BYTES
        || request.data[S547_WORD_BUFFER_SIZE] != S547_PROPERTY_BUFFER_BYTES
    {
        return Err(E::BufferSizeWordDrift);
    }
    if size_word % S547_PROPERTY_BUFFER_ALIGNMENT != 0 {
        return Err(E::BufferSizeNotAligned);
    }
    if request.data[S547_WORD_REQUEST_CODE] != S547_REQUEST_CODE {
        return Err(E::RequestCodeNotZero);
    }
    match response.data[S547_WORD_REQUEST_CODE] {
        S547_RESPONSE_SUCCESS => {}
        S547_RESPONSE_ERROR_PARSING => return Err(E::ResponseErrorParsing),
        _ => return Err(E::ResponseCodeInvalid),
    }
    check_tag_frames(request, response)?;
    if response.data[S547_WORD_END_TAG] != S547_END_TAG
        || request.data[S547_WORD_END_TAG] != S547_END_TAG
    {
        return Err(E::EndTagMissing);
    }
    if response.data[S547_WORD_PADDING] != 0 || request.data[S547_WORD_PADDING] != 0 {
        return Err(E::PaddingNotZero);
    }

    let width = profile.width();
    let height = profile.height();
    let physical = S547_TAG_TABLE[0].first_value_word();
    if request.data[physical] != width
        || request.data[physical + 1] != height
        || response.data[physical] != width
        || response.data[physical + 1] != height
    {
        return Err(E::PhysicalSizeDrift);
    }
    let virtual_size = S547_TAG_TABLE[1].first_value_word();
    if request.data[virtual_size] != width
        || request.data[virtual_size + 1] != height
        || response.data[virtual_size] != width
        || response.data[virtual_size + 1] != height
    {
        return Err(E::VirtualSizeDrift);
    }
    let depth = S547_TAG_TABLE[2].first_value_word();
    if request.data[depth] != S547_DEPTH_BITS || response.data[depth] != S547_DEPTH_BITS {
        return Err(E::DepthDrift);
    }
    let order = S547_TAG_TABLE[3].first_value_word();
    if request.data[order] != S547_PIXEL_ORDER_BGR || response.data[order] != S547_PIXEL_ORDER_BGR {
        return Err(E::PixelOrderDrift);
    }
    let offset = S547_TAG_TABLE[6].first_value_word();
    if request.data[offset] != S547_VIRTUAL_OFFSET_X
        || request.data[offset + 1] != S547_VIRTUAL_OFFSET_Y
        || response.data[offset] != S547_VIRTUAL_OFFSET_X
        || response.data[offset + 1] != S547_VIRTUAL_OFFSET_Y
    {
        return Err(E::VirtualOffsetDrift);
    }

    let allocate = S547_TAG_TABLE[4].first_value_word();
    if request.data[allocate] != S547_ALLOCATE_ALIGNMENT || request.data[allocate + 1] != 0 {
        return Err(E::TagValueSizeDrift);
    }
    let bus_address = response.data[allocate];
    let buffer_size_bytes = response.data[allocate + 1];
    if bus_address == 0 {
        return Err(E::BusAddressZero);
    }
    let arm_physical_address = s547_bus_to_arm_address(bus_address);
    if arm_physical_address == 0 || arm_physical_address % S547_ALLOCATE_ALIGNMENT != 0 {
        return Err(E::ArmAddressMisaligned);
    }
    if buffer_size_bytes == 0 {
        return Err(E::BufferSizeZero);
    }
    let pitch = response.data[S547_TAG_TABLE[5].first_value_word()];
    let minimum_pitch = s547_minimum_pitch(width).ok_or(E::PitchHeightOverflow)?;
    if pitch < minimum_pitch {
        return Err(E::PitchBelowMinimum);
    }
    if pitch % S547_BYTES_PER_PIXEL != 0 {
        return Err(E::PitchNotWordAligned);
    }
    let minimum_size_bytes = pitch.checked_mul(height).ok_or(E::PitchHeightOverflow)?;
    if buffer_size_bytes < minimum_size_bytes {
        return Err(E::BufferSizeBelowMinimum);
    }
    arm_physical_address
        .checked_add(buffer_size_bytes)
        .ok_or(E::AddressRangeOverflow)?;

    Ok(G8lS547FramebufferAllocationReceipt {
        sequence: S547_SEQUENCE,
        predecessor_sequence: S547_EXPECTED_PREDECESSOR,
        r1_stage: S547_R1_STAGE,
        profile,
        width,
        height,
        virtual_width: width,
        virtual_height: height,
        depth_bits: S547_DEPTH_BITS,
        pixel_order: S547_PIXEL_ORDER_BGR,
        virtual_offset_x: S547_VIRTUAL_OFFSET_X,
        virtual_offset_y: S547_VIRTUAL_OFFSET_Y,
        bus_address,
        arm_physical_address,
        buffer_size_bytes,
        pitch,
        minimum_pitch,
        minimum_size_bytes,
        allocate_alignment: S547_ALLOCATE_ALIGNMENT,
        property_buffer_bytes: S547_PROPERTY_BUFFER_BYTES,
        property_channel: S547_PROPERTY_CHANNEL,
        response_code: S547_RESPONSE_SUCCESS,
        tag_count: S547_TAG_COUNT,
        hardware_present: S547_HARDWARE_PRESENT,
        mmio_performed: false,
        s540_physical_verdict_retained_red: S547_S540_PHYSICAL_VERDICT_RETAINED_RED,
        s543_physical_verdict_retained_red: S547_S543_PHYSICAL_VERDICT_RETAINED_RED,
        automatic_promotion: S547_AUTOMATIC_PROMOTION,
        supported_profile_runtime_observations: S547_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS,
        physical_observations: S547_PHYSICAL_OBSERVATIONS,
        boot_to_ui_physically_observed: S547_BOOT_TO_UI_PHYSICALLY_OBSERVED,
        r1_acceptance_complete: S547_R1_ACCEPTANCE_COMPLETE,
        runbook_executed: RUNBOOK_EXECUTED_IN_S547,
    })
}

/// Seed values a later gate would copy into `ui::framebuffer::FramebufferCap`
/// (`phys_addr`, `width`, `height`, `stride`, `format = Bgra8888`).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS547FramebufferCapSeed {
    pub phys_addr: u64,
    pub width: u32,
    pub height: u32,
    pub stride: u32,
    pub format_is_bgra8888: bool,
    pub size_bytes: u64,
}

pub const fn s547_framebuffer_cap_seed(
    receipt: &G8lS547FramebufferAllocationReceipt,
) -> G8lS547FramebufferCapSeed {
    G8lS547FramebufferCapSeed {
        phys_addr: receipt.arm_physical_address as u64,
        width: receipt.width,
        height: receipt.height,
        stride: receipt.pitch,
        format_is_bgra8888: receipt.depth_bits == S547_DEPTH_BITS
            && receipt.pixel_order == S547_PIXEL_ORDER_BGR,
        size_bytes: receipt.buffer_size_bytes as u64,
    }
}

/// Pure allocation service: encodes the request for `profile`, decodes the
/// supplied (modelled) response and publishes one exact receipt.  Exact replay
/// of the same profile and response words is retained; any divergence after
/// publication fails closed.
pub fn service_s547_model_framebuffer_allocation(
    state: &mut G8lS547FramebufferAllocationState,
    profile: G8lS547DisplayProfile,
    response: &G8lS547PropertyBufferWords,
) -> Result<G8lS547FramebufferAllocationOutcome, G8lS547FramebufferAllocationError> {
    let request = encode_s547_framebuffer_request(profile);
    let receipt = decode_s547_framebuffer_response(profile, &request, response)?;
    if let Some(published) = state.receipt {
        if published != receipt
            || state.request != Some(request)
            || state.response != Some(*response)
        {
            return Err(G8lS547FramebufferAllocationError::PublishedStateDrift);
        }
        return Ok(G8lS547FramebufferAllocationOutcome::Retained(published));
    }
    state.receipt = Some(receipt);
    state.request = Some(request);
    state.response = Some(*response);
    Ok(G8lS547FramebufferAllocationOutcome::Allocated(receipt))
}

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

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

const PORTRAIT_BUS: u32 = 0xC000_0000 | 0x3E90_0000;
const PORTRAIT_ARM: u32 = 0x3E90_0000;
const PORTRAIT_PITCH: u32 = 720 * 4;
const PORTRAIT_SIZE: u32 = PORTRAIT_PITCH * 1280;
const HDMI_BUS: u32 = 0xC000_0000 | 0x3D00_0000;
const HDMI_PITCH: u32 = 1920 * 4;
const HDMI_SIZE: u32 = HDMI_PITCH * 1080;

fn portrait_response() -> G8lS547PropertyBufferWords {
    let request = encode_s547_framebuffer_request(G8lS547DisplayProfile::TouchDisplay2Portrait);
    model_s547_firmware_response(&request, PORTRAIT_BUS, PORTRAIT_SIZE, PORTRAIT_PITCH)
}

fn hdmi_response() -> G8lS547PropertyBufferWords {
    let request = encode_s547_framebuffer_request(G8lS547DisplayProfile::HdmiLab1080p);
    model_s547_firmware_response(&request, HDMI_BUS, HDMI_SIZE, HDMI_PITCH)
}

fn allocate(
    state: &mut G8lS547FramebufferAllocationState,
    profile: G8lS547DisplayProfile,
    response: &G8lS547PropertyBufferWords,
) -> Result<G8lS547FramebufferAllocationOutcome, G8lS547FramebufferAllocationError> {
    service_s547_model_framebuffer_allocation(state, profile, response)
}

fn portrait_error(
    mutate: impl FnOnce(&mut [u32; S547_PROPERTY_BUFFER_WORDS]),
) -> Result<G8lS547FramebufferAllocationOutcome, G8lS547FramebufferAllocationError> {
    let mut response = portrait_response();
    mutate(&mut response.data);
    let mut state = G8lS547FramebufferAllocationState::new();
    let result = allocate(
        &mut state,
        G8lS547DisplayProfile::TouchDisplay2Portrait,
        &response,
    );
    assert_eq!(state.receipt(), None);
    result
}

#[test]
fn sequence_scope_and_nonpromotion_are_exact() {
    assert_eq!(S547_SEQUENCE, 547);
    assert_eq!(S547_EXPECTED_PREDECESSOR, 546);
    assert_eq!(S547_R1_STAGE, 2);
    assert_eq!(S547_R1_RANGE_FIRST, 536);
    assert_eq!(S547_R1_RANGE_LAST, 568);
    assert_eq!(S547_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS, 0);
    assert_eq!(S547_PHYSICAL_OBSERVATIONS, 0);
    assert_eq!(S547_PHYSICAL_OR_DEVICE_OPERATIONS, 0);
    assert_eq!(S547_SD_WRITES, 0);
    assert_eq!(S547_UART_OPENS, 0);
    assert_eq!(S547_POWER_TRANSITIONS, 0);
    assert_eq!(S547_NEW_IMMUTABLE_RAW_CAPTURES, 0);
    assert!(S547_S540_PHYSICAL_VERDICT_RETAINED_RED);
    assert!(S547_S543_PHYSICAL_VERDICT_RETAINED_RED);
    assert!(!S547_AUTOMATIC_PROMOTION);
    assert!(!S547_BOOT_TO_UI_PHYSICALLY_OBSERVED);
    assert!(!S547_HARDWARE_PRESENT);
    assert!(!S547_R1_ACCEPTANCE_COMPLETE);
    assert!(!RUNBOOK_EXECUTED_IN_S547);
}

#[test]
fn tag_table_and_word_layout_match_the_mailbox_property_buffer() {
    assert_eq!(S547_PROPERTY_BUFFER_WORDS, 36);
    assert_eq!(S547_PROPERTY_BUFFER_BYTES, 144);
    assert_eq!(S547_PROPERTY_BUFFER_BYTES % S547_PROPERTY_BUFFER_ALIGNMENT, 0);
    assert_eq!(S547_PROPERTY_CHANNEL, 8);
    let expected = [
        (0x0004_8003, 8, 2),
        (0x0004_8004, 8, 7),
        (0x0004_8005, 4, 12),
        (0x0004_8006, 4, 16),
        (0x0004_0001, 8, 20),
        (0x0004_0008, 4, 25),
        (0x0004_8009, 8, 29),
    ];
    let mut next = 2;
    for (descriptor, (tag, bytes, index)) in S547_TAG_TABLE.iter().zip(expected) {
        assert_eq!(descriptor.tag, tag);
        assert_eq!(descriptor.value_bytes, bytes);
        assert_eq!(descriptor.word_index, index);
        assert_eq!(descriptor.word_index, next);
        next = descriptor.end_word();
    }
    assert_eq!(next, S547_WORD_END_TAG);
    assert_eq!(S547_WORD_END_TAG + 2, S547_PROPERTY_BUFFER_WORDS);
    assert_eq!(S547_ALLOCATE_ALIGNMENT, 4096);
    assert_eq!(S547_BUS_TO_ARM_MASK, 0x3FFF_FFFF);
    assert_eq!(S547_DEPTH_BITS, 32);
    assert_eq!(S547_PIXEL_ORDER_BGR, 0);
    assert_eq!(S547_PIXEL_ORDER_RGB, 1);
}

#[test]
fn portrait_request_encodes_exact_words() {
    let words = encode_s547_framebuffer_request(G8lS547DisplayProfile::default()).data;
    let expected: [u32; 36] = [
        144, 0,
        0x0004_8003, 8, 0, 720, 1280,
        0x0004_8004, 8, 0, 720, 1280,
        0x0004_8005, 4, 0, 32,
        0x0004_8006, 4, 0, 0,
        0x0004_0001, 8, 0, 4096, 0,
        0x0004_0008, 4, 0, 0,
        0x0004_8009, 8, 0, 0, 0,
        0, 0,
    ];
    assert_eq!(words, expected);
    let hdmi = encode_s547_framebuffer_request(G8lS547DisplayProfile::HdmiLab1080p).data;
    assert_eq!(hdmi[5], 1920);
    assert_eq!(hdmi[6], 1080);
    assert_eq!(hdmi[10], 1920);
    assert_eq!(hdmi[11], 1080);
    assert_eq!(&hdmi[12..], &expected[12..]);
}

#[test]
fn portrait_touch_display_allocation_publishes_exact_receipt() {
    let mut state = G8lS547FramebufferAllocationState::new();
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) = allocate(
        &mut state,
        G8lS547DisplayProfile::TouchDisplay2Portrait,
        &portrait_response(),
    )
    .unwrap() else {
        panic!("first S547 allocation missing")
    };
    assert_eq!(state.receipt(), Some(receipt));
    assert_eq!(receipt.sequence, 547);
    assert_eq!(receipt.predecessor_sequence, 546);
    assert_eq!(receipt.r1_stage, 2);
    assert_eq!(receipt.profile, G8lS547DisplayProfile::TouchDisplay2Portrait);
    assert_eq!((receipt.width, receipt.height), (720, 1280));
    assert_eq!((receipt.virtual_width, receipt.virtual_height), (720, 1280));
    assert_eq!(receipt.depth_bits, 32);
    assert_eq!(receipt.pixel_order, S547_PIXEL_ORDER_BGR);
    assert_eq!((receipt.virtual_offset_x, receipt.virtual_offset_y), (0, 0));
    assert_eq!(receipt.bus_address, PORTRAIT_BUS);
    assert_eq!(receipt.arm_physical_address, PORTRAIT_ARM);
    assert_eq!(receipt.buffer_size_bytes, PORTRAIT_SIZE);
    assert_eq!(receipt.pitch, 2880);
    assert_eq!(receipt.minimum_pitch, 2880);
    assert_eq!(receipt.minimum_size_bytes, 3_686_400);
    assert_eq!(receipt.allocate_alignment, 4096);
    assert_eq!(receipt.property_buffer_bytes, 144);
    assert_eq!(receipt.property_channel, 8);
    assert_eq!(receipt.response_code, 0x8000_0000);
    assert_eq!(receipt.tag_count, 7);
    assert!(!receipt.hardware_present);
    assert!(!receipt.mmio_performed);
    assert!(receipt.s540_physical_verdict_retained_red);
    assert!(receipt.s543_physical_verdict_retained_red);
    assert!(!receipt.automatic_promotion);
    assert_eq!(receipt.supported_profile_runtime_observations, 0);
    assert_eq!(receipt.physical_observations, 0);
    assert!(!receipt.boot_to_ui_physically_observed);
    assert!(!receipt.r1_acceptance_complete);
    assert!(!receipt.runbook_executed);
}

#[test]
fn hdmi_lab_profile_allocates_1080p_with_padded_pitch() {
    let mut state = G8lS547FramebufferAllocationState::new();
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) =
        allocate(&mut state, G8lS547DisplayProfile::HdmiLab1080p, &hdmi_response()).unwrap()
    else {
        panic!("HDMI allocation missing")
    };
    assert_eq!((receipt.width, receipt.height), (1920, 1080));
    assert_eq!(receipt.pitch, 7680);
    assert_eq!(receipt.arm_physical_address, 0x3D00_0000);
    assert_eq!(receipt.buffer_size_bytes, 8_294_400);

    let request = encode_s547_framebuffer_request(G8lS547DisplayProfile::HdmiLab1080p);
    let padded = model_s547_firmware_response(&request, HDMI_BUS, 8192 * 1080, 8192);
    let mut state = G8lS547FramebufferAllocationState::new();
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) =
        allocate(&mut state, G8lS547DisplayProfile::HdmiLab1080p, &padded).unwrap()
    else {
        panic!("padded HDMI allocation missing")
    };
    assert_eq!(receipt.pitch, 8192);
    assert_eq!(receipt.minimum_pitch, 7680);
    assert_eq!(receipt.minimum_size_bytes, 8192 * 1080);
}

#[test]
fn receipt_seeds_framebuffer_cap_fields() {
    let mut state = G8lS547FramebufferAllocationState::new();
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) = allocate(
        &mut state,
        G8lS547DisplayProfile::TouchDisplay2Portrait,
        &portrait_response(),
    )
    .unwrap() else {
        panic!("allocation missing")
    };
    assert_eq!(
        s547_framebuffer_cap_seed(&receipt),
        G8lS547FramebufferCapSeed {
            phys_addr: 0x3E90_0000,
            width: 720,
            height: 1280,
            stride: 2880,
            format_is_bgra8888: true,
            size_bytes: 3_686_400,
        }
    );
}

#[test]
fn bus_to_arm_conversion_strips_cache_alias_bits() {
    assert_eq!(s547_bus_to_arm_address(0xC000_0000), 0);
    assert_eq!(s547_bus_to_arm_address(0xC3E9_0000), 0x03E9_0000);
    assert_eq!(s547_bus_to_arm_address(0x7E00_B880), 0x3E00_B880);
    assert_eq!(s547_bus_to_arm_address(0xFFFF_FFFF), 0x3FFF_FFFF);
    assert_eq!(s547_bus_to_arm_address(0x1000), 0x1000);
    assert_eq!(s547_minimum_pitch(720), Some(2880));
    assert_eq!(s547_minimum_pitch(1920), Some(7680));
    assert_eq!(s547_minimum_pitch(0x4000_0000), None);
}

#[test]
fn exact_replay_retains_the_same_receipt() {
    let mut state = G8lS547FramebufferAllocationState::new();
    let response = portrait_response();
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) =
        allocate(&mut state, G8lS547DisplayProfile::TouchDisplay2Portrait, &response).unwrap()
    else {
        panic!("first allocation missing")
    };
    assert_eq!(
        allocate(&mut state, G8lS547DisplayProfile::TouchDisplay2Portrait, &response),
        Ok(G8lS547FramebufferAllocationOutcome::Retained(receipt))
    );
    assert_eq!(state.published_response(), Some(response));
    assert_eq!(
        state.published_request(),
        Some(encode_s547_framebuffer_request(G8lS547DisplayProfile::TouchDisplay2Portrait))
    );
}

#[test]
fn divergent_input_after_publication_fails_closed() {
    let mut state = G8lS547FramebufferAllocationState::new();
    let published = allocate(
        &mut state,
        G8lS547DisplayProfile::TouchDisplay2Portrait,
        &portrait_response(),
    )
    .unwrap();
    assert_eq!(
        allocate(&mut state, G8lS547DisplayProfile::HdmiLab1080p, &hdmi_response()),
        Err(G8lS547FramebufferAllocationError::PublishedStateDrift)
    );
    let request = encode_s547_framebuffer_request(G8lS547DisplayProfile::TouchDisplay2Portrait);
    let moved = model_s547_firmware_response(&request, PORTRAIT_BUS + 0x1000, PORTRAIT_SIZE, PORTRAIT_PITCH);
    assert_eq!(
        allocate(&mut state, G8lS547DisplayProfile::TouchDisplay2Portrait, &moved),
        Err(G8lS547FramebufferAllocationError::PublishedStateDrift)
    );
    let G8lS547FramebufferAllocationOutcome::Allocated(receipt) = published else {
        panic!("allocation missing")
    };
    assert_eq!(state.receipt(), Some(receipt));
}

#[test]
fn firmware_error_and_unknown_response_codes_fail_closed() {
    assert_eq!(
        portrait_error(|data| data[S547_WORD_REQUEST_CODE] = S547_RESPONSE_ERROR_PARSING),
        Err(G8lS547FramebufferAllocationError::ResponseErrorParsing)
    );
    for code in [0, 1, 0x8000_0002, 0x7FFF_FFFF, 0xFFFF_FFFF] {
        assert_eq!(
            portrait_error(|data| data[S547_WORD_REQUEST_CODE] = code),
            Err(G8lS547FramebufferAllocationError::ResponseCodeInvalid),
            "code {code:#x}"
        );
    }
}

#[test]
fn buffer_header_and_end_tag_drift_fail_closed() {
    assert_eq!(
        portrait_error(|data| data[S547_WORD_BUFFER_SIZE] = 140),
        Err(G8lS547FramebufferAllocationError::BufferSizeWordDrift)
    );
    assert_eq!(
        portrait_error(|data| data[S547_WORD_BUFFER_SIZE] = 160),
        Err(G8lS547FramebufferAllocationError::BufferSizeWordDrift)
    );
    assert_eq!(
        portrait_error(|data| data[S547_WORD_END_TAG] = 1),
        Err(G8lS547FramebufferAllocationError::EndTagMissing)
    );
    assert_eq!(
        portrait_error(|data| data[S547_WORD_PADDING] = 0xDEAD_BEEF),
        Err(G8lS547FramebufferAllocationError::PaddingNotZero)
    );
}

#[test]
fn tag_frame_drift_fails_closed_per_tag() {
    for descriptor in S547_TAG_TABLE {
        let index = descriptor.word_index;
        assert_eq!(
            portrait_error(|data| data[index] ^= 1),
            Err(G8lS547FramebufferAllocationError::TagIdentifierDrift)
        );
        assert_eq!(
            portrait_error(|data| data[index + 1] += 4),
            Err(G8lS547FramebufferAllocationError::TagValueSizeDrift)
        );
        assert_eq!(
            portrait_error(|data| data[index + 2] &= !S547_TAG_RESPONSE_BIT),
            Err(G8lS547FramebufferAllocationError::TagResponseBitMissing)
        );
        assert_eq!(
            portrait_error(|data| data[index + 2] = S547_TAG_RESPONSE_BIT | (descriptor.value_bytes + 4)),
            Err(G8lS547FramebufferAllocationError::TagResponseLengthDrift)
        );
    }
}

#[test]
fn firmware_echo_drift_of_size_depth_order_and_offset_fails_closed() {
    assert_eq!(
        portrait_error(|data| data[5] = 1080),
        Err(G8lS547FramebufferAllocationError::PhysicalSizeDrift)
    );
    assert_eq!(
        portrait_error(|data| data[11] = 1279),
        Err(G8lS547FramebufferAllocationError::VirtualSizeDrift)
    );
    assert_eq!(
        portrait_error(|data| data[15] = 16),
        Err(G8lS547FramebufferAllocationError::DepthDrift)
    );
    assert_eq!(
        portrait_error(|data| data[19] = S547_PIXEL_ORDER_RGB),
        Err(G8lS547FramebufferAllocationError::PixelOrderDrift)
    );
    assert_eq!(
        portrait_error(|data| data[33] = 1),
        Err(G8lS547FramebufferAllocationError::VirtualOffsetDrift)
    );
}

#[test]
fn allocation_address_and_size_boundaries_fail_closed() {
    assert_eq!(
        portrait_error(|data| data[23] = 0),
        Err(G8lS547FramebufferAllocationError::BusAddressZero)
    );
    assert_eq!(
        portrait_error(|data| data[23] = 0xC000_0000),
        Err(G8lS547FramebufferAllocationError::ArmAddressMisaligned)
    );
    assert_eq!(
        portrait_error(|data| data[23] = PORTRAIT_BUS | 0x10),
        Err(G8lS547FramebufferAllocationError::ArmAddressMisaligned)
    );
    assert_eq!(
        portrait_error(|data| data[24] = 0),
        Err(G8lS547FramebufferAllocationError::BufferSizeZero)
    );
    assert_eq!(
        portrait_error(|data| data[24] = PORTRAIT_SIZE - 1),
        Err(G8lS547FramebufferAllocationError::BufferSizeBelowMinimum)
    );
    assert_eq!(
        portrait_error(|data| {
            data[23] = 0xC000_0000 | 0x3FFF_F000;
            data[24] = 0x0000_2000;
        }),
        Err(G8lS547FramebufferAllocationError::BufferSizeBelowMinimum)
    );
    assert_eq!(
        portrait_error(|data| {
            data[23] = 0xC000_0000 | 0x3FFF_F000;
            data[24] = 0xFFFF_FFFF;
        }),
        Err(G8lS547FramebufferAllocationError::AddressRangeOverflow)
    );
}

#[test]
fn pitch_boundaries_and_overflow_fail_closed() {
    assert_eq!(
        portrait_error(|data| data[28] = 2879),
        Err(G8lS547FramebufferAllocationError::PitchBelowMinimum)
    );
    assert_eq!(
        portrait_error(|data| data[28] = 0),
        Err(G8lS547FramebufferAllocationError::PitchBelowMinimum)
    );
    assert_eq!(
        portrait_error(|data| data[28] = 2882),
        Err(G8lS547FramebufferAllocationError::PitchNotWordAligned)
    );
    assert_eq!(
        portrait_error(|data| data[28] = 0x0040_0000),
        Err(G8lS547FramebufferAllocationError::PitchHeightOverflow)
    );
    assert_eq!(
        portrait_error(|data| data[28] = 0xFFFF_FFFC),
        Err(G8lS547FramebufferAllocationError::PitchHeightOverflow)
    );
    let request = encode_s547_framebuffer_request(G8lS547DisplayProfile::TouchDisplay2Portrait);
    let exact = model_s547_firmware_response(&request, PORTRAIT_BUS, 3072 * 1280, 3072);
    let mut state = G8lS547FramebufferAllocationState::new();
    assert!(matches!(
        allocate(&mut state, G8lS547DisplayProfile::TouchDisplay2Portrait, &exact),
        Ok(G8lS547FramebufferAllocationOutcome::Allocated(receipt)) if receipt.pitch == 3072
    ));
}

#[test]
fn diagnostic_codes_are_nonzero_and_unique() {
    let errors = [
        G8lS547FramebufferAllocationError::BufferSizeWordDrift,
        G8lS547FramebufferAllocationError::BufferSizeNotAligned,
        G8lS547FramebufferAllocationError::RequestCodeNotZero,
        G8lS547FramebufferAllocationError::ResponseErrorParsing,
        G8lS547FramebufferAllocationError::ResponseCodeInvalid,
        G8lS547FramebufferAllocationError::TagIdentifierDrift,
        G8lS547FramebufferAllocationError::TagValueSizeDrift,
        G8lS547FramebufferAllocationError::TagResponseBitMissing,
        G8lS547FramebufferAllocationError::TagResponseLengthDrift,
        G8lS547FramebufferAllocationError::EndTagMissing,
        G8lS547FramebufferAllocationError::PaddingNotZero,
        G8lS547FramebufferAllocationError::PhysicalSizeDrift,
        G8lS547FramebufferAllocationError::VirtualSizeDrift,
        G8lS547FramebufferAllocationError::DepthDrift,
        G8lS547FramebufferAllocationError::PixelOrderDrift,
        G8lS547FramebufferAllocationError::VirtualOffsetDrift,
        G8lS547FramebufferAllocationError::BusAddressZero,
        G8lS547FramebufferAllocationError::ArmAddressMisaligned,
        G8lS547FramebufferAllocationError::BufferSizeZero,
        G8lS547FramebufferAllocationError::PitchBelowMinimum,
        G8lS547FramebufferAllocationError::PitchNotWordAligned,
        G8lS547FramebufferAllocationError::PitchHeightOverflow,
        G8lS547FramebufferAllocationError::BufferSizeBelowMinimum,
        G8lS547FramebufferAllocationError::AddressRangeOverflow,
        G8lS547FramebufferAllocationError::PublishedStateDrift,
    ];
    let codes: BTreeSet<_> = errors
        .into_iter()
        .map(G8lS547FramebufferAllocationError::diagnostic_code)
        .collect();
    assert_eq!(codes.len(), errors.len());
    assert!(!codes.contains(&0));
}

#[test]
fn module_is_registered_in_kernel_and_simulation() {
    let module = "g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s547_r1_display_mailbox_framebuffer_allocation_contract";
    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",
        "read_volatile",
        "crate::uart",
        "crate::arch",
        "#[no_mangle]",
        "spin::",
        "std::",
        "crate::kprintln!",
    ] {
        assert!(!SOURCE.contains(forbidden), "forbidden token: {forbidden}");
    }
    assert!(SOURCE.contains("performs no device operation"));
    assert!(SOURCE.contains("not modify `driver::mailbox`; it only mirrors its `PropertyBuffer` naming"));
}

#[test]
fn source_only_gate_keeps_runtime_physical_and_r1_claims_zero() {
    assert!(SOURCE.contains("S547_SUPPORTED_PROFILE_RUNTIME_OBSERVATIONS: usize = 0"));
    assert!(SOURCE.contains("S547_PHYSICAL_OBSERVATIONS: usize = 0"));
    assert!(SOURCE.contains("S547_PHYSICAL_OR_DEVICE_OPERATIONS: usize = 0"));
    assert!(SOURCE.contains("S547_HARDWARE_PRESENT: bool = false"));
    assert!(SOURCE.contains("S547_BOOT_TO_UI_PHYSICALLY_OBSERVED: bool = false"));
    assert!(SOURCE.contains("S547_R1_ACCEPTANCE_COMPLETE: bool = false"));
    assert!(SOURCE.contains("RUNBOOK_EXECUTED_IN_S547: bool = false"));
}

  {
    id: "g8l-s547-r1-display-mailbox-framebuffer-allocation-contract",
    date: "2026-08-30",
    sequence: 547,
    status: "passed",
    umbrella_status: "partial",
    title: "S547 · R1 ekran: VideoCore mailbox framebuffer tahsis sözleşmesi",
    summary:
      "S547 kaynak/host model kapısı PASS'tir: Raspberry Pi 5 HDMI ilk-piksel yolunun VideoCore property-mailbox framebuffer tahsis işlemi, 36 word / 144 B / 16-byte katlı property buffer düzeni, yedi tag (0x00048003 fiziksel boyut, 0x00048004 sanal boyut, 0x00048005 derinlik 32, 0x00048006 piksel sırası BGR, 0x00040001 tahsis 4096 hizalı, 0x00040008 pitch, 0x00048009 sanal offset), 0x80000000/0x80000001 yanıt kodları, bus→ARM adres dönüşümü (& 0x3FFFFFFF) ve pitch >= width*4 / size >= pitch*height denetimleriyle fail-closed olarak modellendi. Varsayılan hedef 720x1280 portre Touch Display 2 profili, laboratuvar profili 1920x1080 HDMI'dır; her iki profil G8lS547FramebufferAllocationReceipt ve FramebufferCap tohum alanları (phys_addr, width, height, stride, Bgra8888) üretir. Focused 19/19 PASS'tir. S540 ve S543 fiziksel RED immutable kalır; physical observation=0, MMIO=0, donanım yoktur ve RUNBOOK_EXECUTED_IN_S547=NO'dur. S548 bu receipt'ten tohumlanan framebuffer capability'sine host-modelli test deseni bağlama kapısıdır.",
    evidence: [
      "S547, S546'dan ayrı bir source/host model module, 19-test focused binary, proof, status manifest, Operations kaydı ve complete Code kartına sahiptir; hiçbir production callsite, boot/IRQ/scheduler/driver bağlantısı yoktur.",
      "Dar S547 source-model status=PASS; R1 umbrella=PARTIAL ve S540/S543 physical gate status=RED olarak ayrı tutulur.",
      "Property buffer düzeni exact 36 word / 144 B'dir ve driver::mailbox PropertyBuffer data: [u32; 36] adlandırmasını değiştirmeden yansıtır; kanal 8, word 0 boyut, word 1 istek kodu 0, word 34 end tag 0, word 35 padding 0'dır.",
      "Tag tablosu exact word indeksleriyle sabittir: 0x00048003 @2, 0x00048004 @7, 0x00048005 @12 (32 bit), 0x00048006 @16 (BGR=0), 0x00040001 @20 (hizalama 4096), 0x00040008 @25, 0x00048009 @29 (offset 0,0).",
      "Yanıt kodu yalnız 0x80000000 kabul edilir; 0x80000001 firmware parse hatası, diğer her değer geçersiz yanıt kodu olarak fail-closed döner.",
      "Her tag çerçevesinde kimlik, değer boyutu, 0x80000000 yanıt biti ve exact yanıt uzunluğu doğrulanır; zincir word 34'te bitmezse veya padding sıfır değilse reddedilir.",
      "Fiziksel boyut, sanal boyut, derinlik 32, piksel sırası BGR ve sanal offset (0,0) echo'ları exact olmalıdır; herhangi bir sapma ilgili drift hatasını üretir.",
      "Bus adresi sıfır olamaz; ARM adresi bus & 0x3FFFFFFF ile türetilir, sıfır olamaz ve 4096 hizalı olmalıdır; buffer boyutu sıfır olamaz.",
      "pitch >= width*4 (checked çarpma), pitch % 4 == 0, size >= pitch*height (checked çarpma) ve ARM adresi + size u32 taşması denetimleri uygulanır; taşma durumları ayrı diagnostic kodlarıyla reddedilir.",
      "Portre profili 720x1280 için minimum pitch 2880 B ve minimum boyut 3686400 B; HDMI laboratuvar profili 1920x1080 için 7680 B ve 8294400 B'dir; firmware'in daha geniş pitch döndürmesi (örn. 3072 veya 8192) kabul edilir.",
      "Receipt exact bir kez yayımlanır; aynı profil ve aynı yanıt kelimeleriyle replay Retained döner, farklı profil veya yanıt PublishedStateDrift ile fail-closed reddedilir.",
      "Yirmi beş hata varyantının diagnostic kodları sıfırdan farklı ve benzersizdir.",
      "Focused target 1 grup / 19 passed / 0 failed / 0 ignored / 0 filtered verdi.",
      "Implementation 23979 B / ee0cba46519f790f84e18eac133e9bfd8a7b9dd4bf24fe2dc62f8e8f543c1b57; focused test 19792 B / 17bd3072b422e8096e88079a6a3c54ddd54ee9848294ae7d9331af1601e51ca6 SHA-256'dır.",
      "Proof 4740 B'dir.",
      "Kaynak unsafe, asm!, write_volatile, crate::uart, crate::arch, #[no_mangle] veya spin:: içermez; mailbox MMIO yapılmaz ve firmware yanıtı focused test tarafından host üzerinde sentezlenir.",
      "S540 ve S543 immutable raw ve fiziksel RED kararları byte-exact korunur; automatic promotion=false'dur ve S546 kararı varsayılmaz.",
      "RUNBOOK_EXECUTED_IN_S547=NO; supported-profile runtime observations=0, physical observations=0, SD/UART/power/new-raw=0/0/0/0, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.",
      "S548 yalnız host üzerinde S547 receipt'inden tohumlanan framebuffer capability'sine test deseni bağlayacaktır; aygıt 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_s547_r1_display_mailbox_framebuffer_allocation_contract -- --test-threads=1",
    ],
    terminalSessions: [
      {
        id: "s547-focused",
        title: "S547 mailbox framebuffer allocation contract focused",
        commandLines: [
          "CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s547_r1_display_mailbox_framebuffer_allocation_contract -- --test-threads=1",
        ],
        outputLines: [
          "test result: ok. 19 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s",
          "S547 focused=1 group / 19 passed / 0 failed",
          "hardware=none physical=0 runbook=NO",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
    ],
    limitations: [
      "S547 yalnız host üzerinde çalışan bir kaynak modelidir; hiçbir donanım/panel/modem/board gözlemi yoktur ve VideoCore firmware yanıtı sentezlenmiştir.",
      "Mailbox MMIO, framebuffer belleğine yazma veya gerçek piksel çıkışı yapılmamıştır; BOOT_TO_UI_READY gerçek UART'ta görülmedi, Boot-to-UI ve R1 acceptance false kalır.",
      "S540 ve S543 fiziksel RED immutable kalır; S546 üçüncü fiziksel koşunun kararı bu kapıda varsayılmaz veya yükseltilmez.",
      "Modül hiçbir boot, IRQ, scheduler veya driver yoluna bağlı değildir; driver::mailbox değiştirilmemiştir.",
      "S548 host-only test deseni ve capability bağlama kapısıdır; yeni SD/UART/power koşusu ayrı kapı, fresh target revalidation, açık operatör yetkisi ve yeni immutable raw ister.",
    ],
  },