G8k: ASID encoding ve fail-closed TLB shootdown modeli

//! G8k bounded ASID-encoding and fail-closed TLB shootdown model.
//!
//! S161 proves the host-side ordering boundary for one nonzero 8-bit ASID:
//! the production encoder is used, the online CPU mask is snapshotted, every
//! CPU in that snapshot must acknowledge exactly once, and ASID reuse is
//! unavailable until the complete shootdown has been committed.  This is a
//! source/model proof only; it does not claim production scheduler wiring,
//! QEMU execution, or physical RPi5 evidence.

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

pub const CPU_COUNT: usize = 4;
pub const ALL_ONLINE_MASK: u8 = 0b1111;
pub const TEST_ASID: u16 = 37;
pub const TEST_ROOT: u64 = 0x0000_0000_4020_0000;

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

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct AsidReuseReceipt {
    pub asid: u16,
    pub generation: u64,
    pub ttbr0_operand: u64,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum TlbShootdownError {
    Encoding(AsidEncodingError),
    ZeroAsidUnsupported,
    InvalidOnlineMask,
    InvalidCpu,
    CpuNotOnline,
    CpuNotInSnapshot,
    AsidMismatch,
    ShootdownAlreadyActive,
    AsidReusePending,
    StaleTicket,
    DuplicateAck,
    MissingAck,
    OnlineMaskChanged,
    AsidReuseBeforeCompletion,
    AsidReuseNotReleased,
    GenerationOverflow,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Mapping {
    asid: u16,
    root: u64,
    generation: u64,
}

#[test]
fn asid_reuse_is_blocked_until_full_completion_then_advances_generation() {
    let mut model = model();
    let ticket = model.begin_shootdown(TEST_ASID).unwrap();
    assert_eq!(
        model.begin_reuse(TEST_ASID, REUSED_ROOT),
        Err(TlbShootdownError::AsidReuseBeforeCompletion)
    );
    ack_all(&mut model, ticket);
    assert_eq!(
        model.begin_reuse(TEST_ASID, REUSED_ROOT),
        Err(TlbShootdownError::AsidReuseBeforeCompletion)
    );
    model.complete(ticket).unwrap();
    let receipt = model.begin_reuse(TEST_ASID, REUSED_ROOT).unwrap();
    assert_eq!(
        receipt,
        AsidReuseReceipt {
            asid: TEST_ASID,
            generation: 2,
            ttbr0_operand: 0x0025_0000_4040_0000,
        }
    );
    assert_eq!(model.mapping_generation(), 2);
    assert!(!model.asid_reusable());
}

  {
    id: "g8k-asid-tlb-shootdown-model-partial",
    date: "2026-08-24",
    sequence: 161,
    status: "passed",
    umbrella_status: "partial",
    title: "G8k: ASID encoding ve fail-closed TLB shootdown modeli",
    summary:
      "S161, production-owned 8-bit ASID encoder'ı doğrudan kullanarak nonzero ASID37 için ASIDE1=0x0025_0000_0000_0000 ve TTBR0=0x0025_0000_4020_0000 operandlarını exact bağladı; ASID0 ve out-of-range ASID reddedildi. Dört CPU online maskesi snapshot'landı; stale-mapping sentinel her snapshot CPU ACK'ine kadar korundu; ACK 0→1→2→3→4 exact, eksik/çift ACK, snapshot-outsider ACK, forged ACK-mask ve online-mask değişimi mutasyonsuz fail-closed kaldı. ASID reuse hem tam ACK öncesi hem completion commit öncesi reddedildi, commit sonrasında generation 1→2 ile kabul edildi. Reuse release tüketilmeden yeni shootdown açılamadı; tamamlanmış ticket aynı generation'da yeniden canlanamadı. Production TLBI/ASID allocator wiring, QEMU, fiziksel runtime ve generic SMP açık kaldı.",
    evidence: [
      "g8k_tlb_shootdown: 8/8 PASS; production encoder ile ASIDE1=0x0025_0000_0000_0000 ve TTBR0=0x0025_0000_4020_0000 exact doğrulandı.",
      "ASID0/out-of-range admission reddi; dört CPU online-mask snapshot'ı, stale-mapping sentinel ve ACK 0→1→2→3→4 exact kapanışı doğrulandı; missing/duplicate ACK fail-closed kaldı.",
      "Online-mask değişimi completion'ı durdurdu; snapshot-outsider/offline/invalid CPU, foreign, stale, replay, forged ticket ve forged ACK-mask olayları ACK state'ini değiştirmedi.",
      "ASID reuse full completion öncesi reddedildi; completion sonrasında yeni kökle generation 1→2 receipt üretildi. Release tüketilmeden ikinci shootdown reddedildi ve tamamlanmış generation-1 ticket tekrar geçerli olmadı.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8k-S161-ASID-TLB-Shootdown-Model-Proof.md`.",
      "S161 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S161=NO.",
    ],
    commands: [
      "cargo test -p aselsan_microkernel_simulation --test g8k_tlb_shootdown -- --test-threads=1",
    ],
    terminalSessions: [
      {
        id: "s161-g8k-asid-tlb-shootdown-model",
        title: "G8k ASID encoding/TLB shootdown host model kapısı",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test g8k_tlb_shootdown -- --test-threads=1",
        ],
        outputLines: ["running 8 tests", "test result: ok. 8 passed; 0 failed"],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S161 yalnız bounded source/model shootdown sözleşmesidir; production TLBI execution, ASID allocator reuse, scheduler migration, QEMU, fiziksel RPi ve generic SMP runtime sonucu değildir.",
    limitations: [
      "Production TLBI/ASID allocator wiring ve scheduler migration bağlanmadı; bu kapı source/model sınırındadır.",
      "CPU hotplug, long soak, CPU2/CPU3 production arbitration, physical RPi latency ve generic SMP coordination sonraki kapılardır.",
      "QEMU ve fiziksel/device operations kapsam dışıdır; RUNBOOK_EXECUTED_IN_S161=NO.",
    ],
  },