G8l: production migration/TLBI authority source-contract

//! Allocation-free production authority contract for the G8l migration gate.
//!
//! S165 binds the S163 EL0/nonzero-ASID ordering model to the production
//! AArch64 `encode_ttbr0` implementation and to validated shootdown/readback
//! receipts.  This is a source contract only: it does not claim that the
//! scheduler, context switch path, TLBI interrupt path, QEMU, or hardware
//! runtime has been enabled.

use crate::arch::aarch64::asid_encoding::{encode_ttbr0, AsidEncodingError};

pub const CPU0: usize = 0;
pub const CPU1: usize = 1;
pub const ONLINE_MASK: u8 = 0b0011;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct El0MigrationInput {
    pub task_id: u64,
    pub el0: bool,
    pub asid: u16,
    pub root: u64,
    pub address_space_generation: u64,
    pub owner_cpu: usize,
    pub user_progress: u64,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct MigrationTicket {
    pub task_id: u64,
    pub source_cpu: usize,
    pub target_cpu: usize,
    pub asid: u16,
    pub root: u64,
    pub address_space_generation: u64,
    pub generation: u64,
    pub ttbr0_operand: u64,
    pub user_progress_before: u64,
    pub user_progress_after: u64,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct ShootdownReceipt {
    pub asid: u16,
    pub generation: u64,
    pub online_mask: u8,
    pub ack_mask: u8,
}

impl ShootdownReceipt {
    pub fn new(
        asid: u16,
        generation: u64,
        online_mask: u8,
        ack_mask: u8,
    ) -> Result<Self, G8lAuthorityError> {
        if online_mask == 0 || online_mask & !ONLINE_MASK != 0 {
            return Err(G8lAuthorityError::OnlineMaskInvalid);
        }
        if online_mask != ONLINE_MASK {
            return Err(G8lAuthorityError::OnlineMaskChanged);
        }
        if ack_mask != online_mask {
            return Err(G8lAuthorityError::ShootdownIncomplete);
        }
        Ok(Self {
            asid,
            generation,
            online_mask,
            ack_mask,
        })
    }
}

#[test]
fn admission_rejects_el1_zero_asid_zero_generation_and_foreign_owner() {
    assert_eq!(
        G8lMigrationAuthority::new(El0MigrationInput {
            el0: false,
            ..input()
        })
        .unwrap_err(),
        G8lAuthorityError::NotEl0
    );
    assert_eq!(
        G8lMigrationAuthority::new(El0MigrationInput { asid: 0, ..input() }).unwrap_err(),
        G8lAuthorityError::ZeroOrInvalidAsid
    );
    assert_eq!(
        G8lMigrationAuthority::new(El0MigrationInput {
            address_space_generation: 0,
            ..input()
        })
        .unwrap_err(),
        G8lAuthorityError::InvalidAddressSpaceGeneration
    );
    assert_eq!(
        G8lMigrationAuthority::new(El0MigrationInput {
            owner_cpu: CPU1,
            ..input()
        })
        .unwrap_err(),
        G8lAuthorityError::ForeignMutation
    );
    assert_eq!(
        G8lMigrationAuthority::new(El0MigrationInput {
            asid: 256,
            ..input()
        })
        .unwrap_err(),
        G8lAuthorityError::Encoding(AsidEncodingError::AsidOutOfRange)
    );
}

  {
    id: "g8l-s165-production-migration-authority-contract-partial",
    date: "2026-08-24",
    sequence: 165,
    status: "passed",
    umbrella_status: "partial",
    title: "G8l: production migration/TLBI authority source-contract",
    summary:
      "S165, S163 G8l admission modelini production source-contract katmanına bağladı: kernel authority kaynağı production AArch64 encode_ttbr0 fonksiyonunu doğrudan çağırarak exact TTBR0 operandını immutable ticket'a koyuyor; validated shootdown receipt exact online mask/ACK ve ASID-generation bağı taşıyor. 13/13 testte RUNNING0→MIGRATING→READY1→RUNNING1, old-mapping retirement olmadan READY1 ve target ERET yasağı, exact read-back, duplicate shootdown/retirement, foreign/stale/replay ve user-progress/ticket-generation overflow fail-closed kapıları geçti. Erken READY reddinden sonra MIGRATING state'i ve güvenli retirement→READY retry yolu korundu. Production scheduler/context-switch/TLBI runtime henüz açılmadı.",
    evidence: [
      "g8l_authority_contract: 13/13 PASS; exact production encoder binding, receipt mask/ACK validation ve authority state machine doğrulandı.",
      "Shootdown receipt exact online mask 0b0011, ACK, ASID ve generation ile bağlandı; duplicate completion exact-once reddedildi.",
      "Old mapping retirement olmadan READY1 ve target CPU ERET reddedildi; erken READY denemesi MIGRATING state'ini korudu ve retirement sonrası retry geçti.",
      "Duplicate mapping retirement exact-once reddedildi; exact TTBR0/ASID/root/address-space-generation read-back zorunlu tutuldu.",
      "Foreign/stale/replay, wrong mask/read-back ve user-progress/ticket-generation u64::MAX overflow state/owner publication öncesi fail-closed kaldı.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8l-S165-Production-Authority-Contract-Proof.md`.",
      "S165 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S165=NO.",
    ],
    commands: ["cargo test --test g8l_authority_contract -- --test-threads=1"],
    terminalSessions: [
      {
        id: "s165-g8l-production-migration-authority-contract",
        title: "G8l production migration/TLBI authority source-contract kapısı",
        commandLines: [
          "cargo test --test g8l_authority_contract -- --test-threads=1",
        ],
        outputLines: [
          "running 13 tests",
          "test result: ok. 13 passed; 0 failed",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S165 source-contract PASS'tir; receipt constructor'ları bounded validated inputs'tur ve production-unforgeable hardware authority receipt değildir. Scheduler/context-switch/TLBI runtime, QEMU, fiziksel RPi ve generic SMP sonucu değildir.",
    limitations: [
      "S163'ün G8j/G8k physical prerequisites closed sınırı korunur; S165 fiziksel PASS üretmez.",
      "Production encoder source'a bağlanmıştır; production scheduler/context-switch migration runtime ve actual TLBI/IRQ authority wiring henüz yoktur.",
      "ShootdownReceipt ve Ttbr0Readback source-contract constructor'larıdır; hardware-derived unforgeable authority kanıtı değildir.",
      "QEMU, physical/device operations, CPU2/CPU3, hotplug, generic SMP arbitration ve soak kapsam dışıdır; RUNBOOK_EXECUTED_IN_S165=NO.",
    ],
  },