G8l: EL0/nonzero-ASID migration admission ve capture modeli

//! G8l EL0/nonzero-ASID migration admission and capture model.
//!
//! S163 deliberately keeps the physical G8j/G8k prerequisites closed.  A
//! synthetic host fixture may open both boolean prerequisites to exercise the
//! ordering contract, but that is not physical PASS evidence or production
//! scheduler wiring.

use crate::aarch64_asid_encoding::{encode_ttbr0, AsidEncodingError};

pub const CPU0: usize = 0;
pub const CPU1: usize = 1;
pub const ONLINE_MASK: u8 = 0b0011;
pub const TEST_TASK: u64 = 73;
pub const TEST_ASID: u16 = 37;
pub const TEST_ROOT: u64 = 0x0000_0000_4020_0000;
pub const TEST_PROGRESS: u64 = 7;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct PhysicalPrerequisites {
    pub g8j_physical_pass: bool,
    pub g8k_physical_pass: bool,
}

impl PhysicalPrerequisites {
    pub const fn closed() -> Self {
        Self {
            g8j_physical_pass: false,
            g8k_physical_pass: false,
        }
    }

    pub const fn synthetic_pass_fixture() -> Self {
        Self {
            g8j_physical_pass: true,
            g8k_physical_pass: true,
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct El0Task {
    pub 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 shootdown_generation: u64,
    pub ttbr0_operand: u64,
    pub user_progress: u64,
}

#[test]
fn shootdown_completion_is_exactly_once_and_duplicate_input_is_transactional() {
    let mut model = model();
    let ticket = model.begin_migration(CPU0, TEST_TASK).unwrap();
    model
        .complete_shootdown(ticket, completion(ticket))
        .unwrap();
    assert_eq!(
        model.complete_shootdown(ticket, completion(ticket)),
        Err(G8lMigrationError::ShootdownAlreadyCompleted)
    );
    assert_eq!(model.state(), MigrationState::Migrating);
    assert!(model.shootdown_completed());
    assert_eq!(model.active_ticket(), Some(ticket));
}

  {
    id: "g8l-el0-nonzero-asid-migration-admission-model-partial",
    date: "2026-08-24",
    sequence: 163,
    status: "passed",
    umbrella_status: "partial",
    title: "G8l: EL0/nonzero-ASID migration admission ve capture modeli",
    summary:
      "S163, EL0 migration admission kapısını 13/13 bounded source/model seviyesinde kapattı: yalnız EL0, nonzero 8-bit ASID, nonzero address-space generation ve CPU0 sahibi görev kabul edildi; production encode_ttbr0 ile exact TTBR0 operandı migration ticket'ına bağlandı. Task, ASID, root, address-space generation, shootdown generation, TTBR0 ve user progress tek immutable capture içinde taşındı. RUNNING0→MIGRATING→READY1→RUNNING1 sırası; exact online mask/ACK, exact TTBR0 read-back, old-mapping retirement öncesi ERET yasağı, foreign/stale/wrong-task, yanlış read-back, replay ve generation overflow fail-closed doğrulandı. Duplicate shootdown completion exact-once reddedildi; user-progress u64::MAX taşması ticket veya ownership yayımlanmadan kapandı. G8j ve G8k fiziksel önkoşulları kapalıdır; testler yalnız açıkça adlandırılmış synthetic fixture kullanır. Production scheduler/context-switch/TLBI, QEMU, fiziksel RPi ve generic SMP açık kaldı.",
    evidence: [
      "g8l_migration: 13/13 PASS; EL0/nonzero 8-bit ASID/address-space generation admission ve production TTBR0 capture binding doğrulandı.",
      "Exact shootdown completion, online-mask/ACK, TTBR0/ASID/root/generation read-back ve monotonic user progress sırası doğrulandı.",
      "Old mapping target CPU ERET öncesi retired; foreign/stale/wrong-task, wrong read-back, replay ve generation overflow state değiştirmeden reddedildi.",
      "Duplicate shootdown completion state değiştirmeden reddedildi; user-progress u64::MAX taşması ticket/owner yayımından önce transactional kapandı.",
      "G8j/G8k physical prerequisites closed; synthetic pass fixture yalnız bounded ordering modelini çalıştırdı.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8l-S163-EL0-Nonzero-ASID-Migration-Admission-Proof.md`.",
      "S163 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S163=NO.",
    ],
    commands: ["cargo test --test g8l_migration -- --test-threads=1"],
    terminalSessions: [
      {
        id: "s163-g8l-el0-nonzero-asid-migration-admission-model",
        title: "G8l EL0/nonzero-ASID migration admission host model kapısı",
        commandLines: ["cargo test --test g8l_migration -- --test-threads=1"],
        outputLines: [
          "running 13 tests",
          "test result: ok. 13 passed; 0 failed",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S163 bounded source/model admission ve capture kapısıdır; physical prerequisites closed, synthetic fixture only. Production scheduler migration, context-switch assembly, TLBI execution, QEMU, fiziksel RPi ve generic SMP runtime sonucu değildir.",
    limitations: [
      "G8j ve G8k fiziksel önkoşulları kapalıdır; modelin default fixture'ı fiziksel PASS üretmez.",
      "PhysicalPrerequisites, ShootdownCompletion ve Ttbr0Readback bounded model girdileridir; fiziksel/S161/hardware authority kaynaklarından production-unforgeable receipt değildir.",
      "Production scheduler/context-switch/TLBI wiring, migration runtime, QEMU, fiziksel RPi, CPU hotplug, CPU2/CPU3 arbitration ve generic SMP koordinasyonu sonraki kapılardır.",
      "QEMU ve fiziksel/device operations kapsam dışıdır; RUNBOOK_EXECUTED_IN_S163=NO.",
    ],
  },