G8l: production IRQ/TLBI receipt wiring boundary

/// Logical receipt channel reserved for the G8l TLBI hand-off.
///
/// S167 does not claim that this channel is enabled in the live GIC path.
pub const G8L_TLBI_RECEIPT_CHANNEL: u32 = 1;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lIrqTlbiWiringInput {
    pub ticket: MigrationTicket,
    pub context_generation: u64,
    pub source_cpu: usize,
    pub target_cpu: usize,
    pub receipt_channel: u32,
    pub online_mask: u8,
    pub irqs_masked: bool,
    pub scheduler_mutation_frozen: bool,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct TlbiRequest {
    pub ticket: MigrationTicket,
    pub context_generation: u64,
    pub source_cpu: usize,
    pub target_cpu: usize,
    pub receipt_channel: u32,
    pub online_mask: u8,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct TlbiAck {
    pub request: TlbiRequest,
    pub ack_cpu: usize,
    pub online_mask: u8,
    pub ack_mask: u8,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum WiringPhase {
    Prepared,
    Ttbr0Installed,
    TlbiRequested,
    Acked,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lIrqTlbiWiringError {
    InvalidContextGeneration,
    InvalidCpu,
    InvalidReceiptChannel,
    OnlineMaskInvalid,
    OnlineMaskChanged,
    IrqMaskRequired,
    SchedulerMutationMustBeFrozen,
    InvalidPhase,
    StaleTicket,
    Ttbr0OperandMismatch,
    RequestMismatch,
    AckCpuMismatch,
    AckMaskMismatch,
    DuplicateAck,
    RuntimePhaseMismatch,
    RuntimeContextGenerationMismatch,
    RuntimeInputMismatch,
    Authority(G8lAuthorityError),
    Runtime(G8lRuntimeError),
}

#[test]
fn request_is_bound_to_source_target_context_channel_and_mask() {
    let mut runtime = authority();
    let ticket = prepared(&mut runtime);
    let mut adapter = wiring(&runtime, ticket);
    let request = requested(&mut runtime, &mut adapter, ticket);
    assert_eq!(request.ticket, ticket);
    assert_eq!(request.context_generation, CONTEXT_GENERATION);
    assert_eq!(request.source_cpu, CPU0);
    assert_eq!(request.target_cpu, CPU1);
    assert_eq!(request.receipt_channel, G8L_TLBI_RECEIPT_CHANNEL);
    assert_eq!(request.online_mask, ONLINE_MASK);
    assert_eq!(adapter.phase(), WiringPhase::TlbiRequested);
}

  {
    id: "g8l-s167-irq-tlbi-receipt-wiring-boundary-partial",
    date: "2026-08-24",
    sequence: 167,
    status: "passed",
    umbrella_status: "partial",
    title: "G8l: production IRQ/TLBI receipt wiring boundary",
    summary:
      "S167, S166 ticket'ını üretim ağacındaki allocation-free IRQ/TLBI receipt boundary'ye bağlayan 14/14 source-contract kapısını kapattı: exact aktif S166 runtime/ticket/context generation, CPU0→CPU1 hedefi, logical receipt channel=1, exact online mask 0b0011, IRQ-masked + scheduler-mutation-frozen guard'ları, production TTBR0 operandı ve TTBR0 kurulumu→TLBI request→CPU1 exact ACK sırası tek adapter'da bağlandı. Adapter construction `SwitchPrepared`, TTBR0/request `Ttbr0Installed` ve receipt delivery aynı aktif runtime kimliğini yeniden doğruluyor. Stale ticket, wrong operand, erken request, yanlış CPU/kanal/mask, duplicate ACK ve başka runtime'dan byte-eşdeğer ticket/context replay'i fail-closed kaldı; hatalı request/ACK sonrası retry liveness korundu. Gerçek GIC/SGI delivery, TLBI instruction, scheduler/context-switch assembly, QEMU ve fiziksel runtime wiring açılmadı.",
    evidence: [
      "g8l_irq_tlbi_wiring: 14/14 PASS; exact S166 migration ticket, TTBR0 operand, context generation, CPU0→CPU1, channel=1 ve mask=0b0011/ACK boundary.",
      "Adapter receipt'i yalnız TTBR0 install sonrasında ve CPU1'in exact online/ACK maskesiyle yayınlıyor; duplicate ACK, stale ticket, wrong operand ve early request state değiştirmeden reddediliyor.",
      "Üretilen ShootdownReceipt yalnız aynı aktif S166 runtime/ticket/context bağı üzerinden complete_tlbi sınırından geçirilerek ShootdownComplete'e ilerledi; farklı context generation taşıyan ikinci runtime reddedildi.",
      "Hatalı request/ACK denemeleri adapter state'ini değiştirmedi ve exact retry başarıyla tamamlandı.",
      "Kanonik focused log: 129 B / d50e861f1dfd8fdd2073cabf26227d26186302c2793942941ffd436c5ff90d25; iki tekrar byte/SHA eşit.",
      "Production board-rpi5 source check başarıyla tamamlandı; yalnız mevcut workspace warning'leri kaldı.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8l-S167-IRQ-TLBI-Receipt-Wiring-Boundary-Proof.md`.",
      "S167 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S167=NO.",
    ],
    commands: [
      "cargo test --quiet --test g8l_irq_tlbi_wiring -- --test-threads=1",
      "cargo check -p aselsan_kernel --no-default-features --features board-rpi5 --target aarch64-unknown-none",
    ],
    terminalSessions: [
      {
        id: "s167-g8l-irq-tlbi-receipt-wiring-boundary",
        title: "G8l S167 IRQ/TLBI receipt wiring boundary",
        commandLines: [
          "cargo test --quiet --test g8l_irq_tlbi_wiring -- --test-threads=1",
        ],
        outputLines: [
          "running 14 tests",
          "test result: ok. 14 passed; 0 failed",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s167-g8l-production-board-rpi5-check",
        title: "G8l S167 board-rpi5 production source check",
        commandLines: [
          "cargo check -p aselsan_kernel --no-default-features --features board-rpi5 --target aarch64-unknown-none",
        ],
        outputLines: ["Finished successfully; existing warnings only"],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S167 source boundary PASS'tir; adapter receipt'i aynı aktif S166 runtime/ticket/context bağı doğrulandıktan sonra bounded source input olarak authority'ye taşır. Gerçek GIC/TLBI instruction, scheduler/context-switch assembly, QEMU, fiziksel RPi ve generic SMP runtime sonucu değildir.",
    limitations: [
      "Production-tree adapter gerçek SGI/GIC delivery veya TLBI instruction çalıştırmaz; hardware-derived unforgeable receipt kanıtı değildir.",
      "Scheduler runtime, context-switch assembly, CPU2/CPU3, hotplug, generic SMP arbitration, QEMU ve soak kapsam dışıdır.",
      "S167 fiziksel/device operasyonu yapmadı; RUNBOOK_EXECUTED_IN_S167=NO.",
    ],
  },