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: cf31620ccc36…file 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: b1b8e2238aaf…file 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: 7aad41cdae81…file sha256: 9726dbf00f84…
Focused test komutu
cargo test --quiet --test g8l_target_dispatch_admission -- --test-threads=1proof: 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