ASELSANMicrokernel
S173 · SOURCE-BOUND GATE EVIDENCE

G8l: target-dispatch CPU1 admission token source boundary

Operations --test hedefi → test hedefiyle aynı adlı uygulama/model modülü → kaynak kesiti Bu sayfa yalnız S173 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S173Focused kod testiOperations id exactsource SHA exacttest target exact

operation: g8l-s173-target-dispatch-admission-partial

uygulama/model · focused test · Operations · 3 exact excerpt

sequence-bound=true · implementation-bound=false
01 · Testin bağlı olduğu uygulama/model kodu

Kapının yürüttüğü gerçek kaynak

tam Rust öğesiL13–L124
kernel/src/g8l_target_dispatch_admission.rs::G8lTargetDispatchAdmissionError
use crate::g8l_target_aarch64_dispatch::G8lTargetAarch64DispatchRoute;
use crate::g8l_target_dispatch_handoff::{G8lTargetDispatchHandoff, G8lTargetDispatchHandoffError};

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lTargetDispatchAdmissionError {
    Handoff(G8lTargetDispatchHandoffError),
    WrongExecutionCpu,
    RuntimeStateMismatch,
}

impl From<G8lTargetDispatchHandoffError> for G8lTargetDispatchAdmissionError {
    fn from(error: G8lTargetDispatchHandoffError) -> Self {
        Self::Handoff(error)
    }
}

#[derive(Debug, PartialEq, Eq)]
pub struct G8lTargetDispatchAdmissionToken {
    runtime_instance_id: u64,
    ticket: MigrationTicket,
    context_generation: u64,
    required_execution_cpu: usize,
    target_route: G8lTargetAarch64DispatchRoute,
    wiring: G8lIrqTlbiWiring,
    live_cpu1_callsite_wired: bool,
}

impl G8lTargetDispatchAdmissionToken {
    /// Consume one exact S172 handoff and retain its authorities for a future
    /// target-only callsite. No target instruction is executed here.
    pub fn from_handoff(
        runtime: &G8lRuntimeAuthority,
        handoff: G8lTargetDispatchHandoff,
        execution_cpu: usize,
    ) -> Result<Self, G8lTargetDispatchAdmissionError> {
        if execution_cpu != CPU1 {
            return Err(G8lTargetDispatchAdmissionError::WrongExecutionCpu);
        }
        handoff.validate_bounded_execution_cpu(execution_cpu)?;
        let runtime_instance_id = handoff.runtime_instance_id();
        if runtime_instance_id == 0 || runtime.instance_id() != runtime_instance_id {
            return Err(G8lTargetDispatchAdmissionError::Handoff(
                G8lTargetDispatchHandoffError::RuntimeInstanceMismatch,
            ));
        }
        let ticket = handoff.ticket();
        let context_generation = handoff.context_generation();
        if runtime.phase() != RuntimePhase::Ttbr0Installed
            || runtime.active_ticket() != Some(ticket)
            || runtime.context_generation() != context_generation
        {
            return Err(G8lTargetDispatchAdmissionError::RuntimeStateMismatch);
        }
        let (target_route, wiring) = handoff.into_sources();
        Ok(Self {
            runtime_instance_id,
            ticket,
            context_generation,
            required_execution_cpu: CPU1,
            target_route,
            wiring,
            live_cpu1_callsite_wired: false,
        })
    }

    pub const fn runtime_instance_id(&self) -> u64 {
        self.runtime_instance_id
    }

    pub const fn ticket(&self) -> MigrationTicket {
        self.ticket
    }

    pub const fn context_generation(&self) -> u64 {
        self.context_generation
    }

    pub const fn required_execution_cpu(&self) -> usize {
        self.required_execution_cpu
    }

    /// Return the retained authorities exactly once by consuming the token.
    /// This transfer remains source-only and does not perform delivery. The
    /// token itself offers no pre-consumption by-value source getters.
    ///
    /// The returned S171/S167 records are still `Copy` bounded source-model
    /// values, so this does not claim globally linear or unforgeable runtime
    /// authority.
    pub fn into_sources(self) -> (G8lTargetAarch64DispatchRoute, G8lIrqTlbiWiring) {
        (self.target_route, self.wiring)
    }

    pub const fn global_source_linearity_proven(&self) -> bool {
        false
    }

    pub const fn live_cpu1_callsite_wired(&self) -> bool {
        self.live_cpu1_callsite_wired
    }

    pub const fn gic_delivery_wired(&self) -> bool {
        false
    }

    pub const fn scheduler_runtime_wired(&self) -> bool {
        false
    }

    pub const fn hardware_execution_proven(&self) -> bool {
        false
    }
}
snippet sha256: cf31620ccc36file sha256: a6751f9a9b2f
02 · Doğrulayan test kodu

Operations komutuna bağlı focused test

tam Rust öğesiL141–L154
simulation/tests/g8l_target_dispatch_admission.rs::token_rejects_foreign_runtime_even_when_handoff_is_value_valid

#[test]
fn token_rejects_foreign_runtime_even_when_handoff_is_value_valid() {
    let (runtime, handoff) = handoff();
    let (foreign, _, _) = sources();
    assert_ne!(runtime.instance_id(), foreign.instance_id());
    assert_eq!(
        G8lTargetDispatchAdmissionToken::from_handoff(&foreign, handoff, CPU1),
        Err(G8lTargetDispatchAdmissionError::Handoff(
            aselsan_microkernel_simulation::g8l_target_dispatch_handoff::
                G8lTargetDispatchHandoffError::RuntimeInstanceMismatch,
        ))
    );
}
snippet sha256: b1b8e2238aaffile sha256: 8e708f30d750
03 · Kapı kimlik kaydı

Operations sıra, kimlik ve başlık bağı

tam Operations kaydıL22946–L22987
website/src/lib/operations.ts::g8l-s173-target-dispatch-admission-partial
  {
    id: "g8l-s173-target-dispatch-admission-partial",
    date: "2026-08-24",
    sequence: 173,
    status: "passed",
    umbrella_status: "partial",
    title: "G8l: target-dispatch CPU1 admission token source boundary",
    summary:
      "S173, exact S172 target-dispatch handoff'unu tüketerek gelecek target-only CPU1 callsite'ı için typed admission token üretti. Admission anında aynı nonzero S166 runtime-instance yanında güncel Ttbr0Installed phase, active ticket ve context generation yeniden doğrulanır; CPU0, foreign runtime ve handoff sonrası ilerlemiş stale runtime fail-closed reddedilir. Token tüketilmeden S171 route/S167 wiring için public by-value getter yoktur. Alttaki iki source record hâlâ Copy olduğu için global lineer veya unforgeable authority kanıtı iddia edilmez. Token source-only'dir: target instruction, live CPU1 callsite, GIC/SGI, scheduler ownership, QEMU veya fiziksel runtime açılmadı.",
    evidence: [
      "g8l_target_dispatch_admission: 5/5 PASS; exact S172 handoff consumption, typed CPU1 token, CPU0/foreign-runtime/stale-advanced-runtime reject ve source audit.",
      "Token route phase TlbiIssued ve wiring phase TlbiRequested değerlerini korurken admission anında runtime Ttbr0Installed phase, active ticket ve context generation değerlerini exact yeniden denetler.",
      "`into_sources` token tüketilerek transfer yapar ve token üzerinde pre-consumption public by-value route/wiring getter yoktur; underlying S171/S167 source record'ları Copy kaldığından global source linearity proven=false.",
      "Kalıcı kapsam: `docs/M8.1-RPi5-G8l-S173-Target-Dispatch-Admission-Proof.md`.",
      "S173 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S173=NO.",
    ],
    commands: [
      "cargo test --quiet --test g8l_target_dispatch_admission -- --test-threads=1",
      "cargo check -p aselsan_kernel --no-default-features --features board-rpi5 --target aarch64-unknown-none",
    ],
    terminalSessions: [
      {
        id: "s173-g8l-target-dispatch-admission",
        title: "G8l S173 target-dispatch admission source boundary",
        commandLines: [
          "cargo test --quiet --test g8l_target_dispatch_admission -- --test-threads=1",
        ],
        outputLines: ["running 5 tests", "test result: ok; 5 passed; 0 failed"],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S173 typed token PASS'tir; token future callsite authority'sini taşır fakat execution, GIC/SGI veya scheduler-owned migration runtime kanıtı değildir.",
    limitations: [
      "S173 host'ta target-only unsafe AArch64 instruction veya live CPU1 delivery callsite çalıştırmaz.",
      "CPU1 admission bounded, hardware-derived olmayan bir girdidir; eventual S171 callsite production MPIDR kimliğini yeniden doğrulamalıdır.",
      "Token public by-value source getter sunmaz; fakat alttaki S171/S167 source record'ları Copy olduğu için global lineer/unforgeable authority kanıtlanmış değildir.",
      "Token SGI/GIC'e dokunmaz, scheduler ownership/context-switch assembly mutasyonu yapmaz.",
      "S173 fiziksel/device operasyonu yapmadı; RUNBOOK_EXECUTED_IN_S173=NO.",
    ],
  },
snippet sha256: 7aad41cdae81file sha256: 9726dbf00f84
Focused test komutu
cargo test --quiet --test g8l_target_dispatch_admission -- --test-threads=1
proof: docs/M8.1-RPi5-G8l-S173-Target-Dispatch-Admission-Proof.md
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9