G8j: EL1 shared-root/ASID0 migration round-trip modeli

//! G8j bounded CPU0→CPU1→CPU0 migration round-trip model.
//!
//! S160 keeps the S159 admission boundary unchanged: static EL1, shared root,
//! ASID 0 and one task.  It adds a second, separately ticketed return leg and
//! never claims production scheduler, assembly, QEMU, or physical runtime.

pub const CPU0: usize = 0;
pub const CPU1: usize = 1;
pub const SHARED_ROOT_ID: u64 = 1;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum RoundTripState {
    Running0,
    MigratingForward,
    Ready1,
    Running1,
    MigratingBack,
    Ready0,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct RoundTripTask {
    pub id: u64,
    pub is_static: bool,
    pub el0: bool,
    pub asid: u16,
    pub root_id: u64,
    pub owner_cpu: usize,
    pub stack_owner_cpu: usize,
    pub stack_generation: u64,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct RoundTripTicket {
    pub task_id: u64,
    pub generation: u64,
    pub stack_generation: u64,
    pub source_cpu: usize,
    pub target_cpu: usize,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum RoundTripError {
    InvalidCpu,
    ForeignMutation,
    WrongTask,
    DuplicateExecution,
    InvalidState,
    StaleRequest,
    TaskLost,
    InvalidDescriptor,
    StackGenerationNotMonotonic,
    StackOwnershipAmbiguous,
}

#[test]
fn final_round_trip_has_one_owner_and_monotonic_ticket_generations() {
    let mut model = G8jRoundTripModel::new();
    model.start_running0(task(13)).unwrap();
    let forward = model.begin_forward(CPU0, 13).unwrap();
    model.publish_forward(CPU0, forward).unwrap();
    model.start_running1(CPU1, forward).unwrap();
    let reverse = model.begin_reverse(CPU1, 13).unwrap();
    assert_eq!(reverse.generation, forward.generation + 1);
    model.publish_reverse(CPU1, reverse).unwrap();
    model.finish_running0(CPU0, reverse).unwrap();
    let final_task = model.task().unwrap();
    assert_eq!(final_task.id, 13);
    assert_eq!(final_task.owner_cpu, CPU0);
    assert_eq!(final_task.stack_owner_cpu, CPU0);
    assert_eq!(final_task.stack_generation, 3);
    assert_eq!(model.active_ticket(), None);
}

  {
    id: "g8j-el1-asid0-round-trip-model-partial",
    date: "2026-08-24",
    sequence: 160,
    status: "passed",
    umbrella_status: "partial",
    title: "G8j: EL1 shared-root/ASID0 migration round-trip modeli",
    summary:
      "S160, S159'un explicit static/EL1/shared-root id=1/ASID0 admission sınırını koruyarak CPU0→CPU1→CPU0 round-trip'i 8/8 bounded host/model seviyesinde kapattı: RUNNING0→MIGRATING_FORWARD→READY1→RUNNING1→MIGRATING_BACK→READY0→RUNNING0, iki ayrı ticket generation, exact task/IRQ-stack owner dönüşü 0→1→0, stack generation 1→2→3 ve task loss/çift execution yokluğu. Her bacak stack rotation'ı ticket öncesi preflight ediyor; owner/stack/generation publish tek transaction. MAX-1→MAX sonrası reverse başlangıcı mutasyonsuz reddedildi. Production migration, ASID/TLB shootdown, EL0/nonzero-ASID, QEMU ve fiziksel runtime açık kaldı.",
    evidence: [
      "g8j_round_trip: 8/8 PASS; explicit static/EL1/shared-root id=1/ASID0 descriptor, dynamic/private-root reddi ve iki bacak exact state chain doğrulandı.",
      "Forward CPU0→CPU1 ve reverse CPU1→CPU0 owner transferleri exact; stack generation 1→2→3, ticket generation 1→2 ve her RUNNING commit'inde retirement geçti.",
      "Per-leg stack-rotation preflight ve hesapla-sonra-commit owner/stack/generation publication doğrulandı; u64::MAX reverse sınırı state/task/ticket/counter değiştirmedi.",
      "Task round-trip sonunda CPU0'da tek owner olarak kaldı; task loss ve concurrent execution oluşmadı.",
      "Foreign mutation, iki bacak stale/replay ticket, forward/reverse wrong task, forged stack generation, invalid CPU/descriptor ve EL0/nonzero-ASID sınırları mutasyonsuz reddedildi.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8j-S160-EL1-ASID0-Round-Trip-Model-Proof.md`.",
      "S160 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S160=NO.",
    ],
    commands: [
      "cargo test -p aselsan_microkernel_simulation --test g8j_round_trip -- --test-threads=1",
    ],
    terminalSessions: [
      {
        id: "s160-g8j-el1-asid0-round-trip-model",
        title: "G8j EL1/ASID0 migration round-trip host model kapısı",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test g8j_round_trip -- --test-threads=1",
        ],
        outputLines: ["running 8 tests", "test result: ok. 8 passed; 0 failed"],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S160 yalnız bounded source/model round-trip sözleşmesidir; production scheduler migration, context-switch assembly, ASID/TLB shootdown, EL0/nonzero-ASID, QEMU, fiziksel RPi ve generic SMP runtime sonucu değildir.",
    limitations: [
      "Production migration/context-switch wiring ve ASID/TLB shootdown bağlanmadı; bu kapı source/model sınırındadır.",
      "EL0/nonzero-ASID migration, CPU2/CPU3, hotplug, long soak ve generic SMP arbitration sonraki kapılardır.",
      "QEMU ve fiziksel/device operations kapsam dışıdır; RUNBOOK_EXECUTED_IN_S160=NO.",
    ],
  },