S412 · SOURCE-BOUND GATE EVIDENCE
S412 · Exclusion-gated join preflight
tam S412 implementation modülü → Operations --test hedefi ile bağlı tam focused test → ayrı Operations kaydı Bu sayfa yalnız S412 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.
S412Focused kod testiOperations id exactsource SHA exacttest target exact
operation: g8l-s412-exclusion-gated-join-preflight-partial
uygulama/model · focused test · Operations · 3 exact excerpt
sequence-bound=true · implementation-bound=true
01 · Yürütme / doğrulama kodu
Kapının gerçek repository sözleşmesi
tam dosyaL1–L153
kernel/src/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight.rs::S412 exclusion gated join preflight implementation
#![allow(unexpected_cfgs)]
//! S412 non-consuming four-way exclusion-gated join preflight.
//!
//! The S411 admission, its still-live S247 token, returned S242 authorities,
//! the S240 post-EOI receipt, and free S243 output capacity must all agree
//! before the next gate may consume anything. S412 only reads those surfaces;
//! it neither takes a linear value nor enters S243.
use crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s411_ephemeral_exclusion_admission_constructor::{
G8lS411EphemeralExclusionAdmissionError, G8lS411EphemeralExclusionAdmissionView,
S411_DIRECT_SCHEDULER_ACCESS_SITES, S411_PRODUCTION_GUARDED_DIRECT_ACCESS_SITES,
S411_SOURCE_AUDIT_UNITS, S411_SOURCE_MODEL_COVERED_DIRECT_ACCESS_SITES,
S411_UNROUTED_DIRECT_ACCESS_SITES,
};
pub const S412_SOURCE_AUDIT_UNITS: usize = S411_SOURCE_AUDIT_UNITS;
pub const S412_DIRECT_SCHEDULER_ACCESS_SITES: usize = S411_DIRECT_SCHEDULER_ACCESS_SITES;
pub const S412_SOURCE_MODEL_COVERED_DIRECT_ACCESS_SITES: usize =
S411_SOURCE_MODEL_COVERED_DIRECT_ACCESS_SITES;
pub const S412_PRODUCTION_GUARDED_DIRECT_ACCESS_SITES: usize =
S411_PRODUCTION_GUARDED_DIRECT_ACCESS_SITES;
pub const S412_UNROUTED_DIRECT_ACCESS_SITES: usize = S411_UNROUTED_DIRECT_ACCESS_SITES;
pub const S412_PRODUCTION_PREFLIGHT_CALLSITES: usize = 1;
pub const S412_LINEAR_INPUT_TAKE_SITES: usize = 0;
pub const S412_PRODUCTION_S243_JOIN_CALLSITES: usize = 0;
pub const S412_FOUR_WAY_READINESS_PREFLIGHT_COMPLETE: bool = true;
pub const S412_END_TO_END_EXCLUSION_ADMISSION_COMPLETE: bool = false;
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct G8lS412ExclusionGatedJoinPreflightReceipt {
attempt_id: u64,
provider_request_id: u64,
exclusive_token: u64,
}
impl G8lS412ExclusionGatedJoinPreflightReceipt {
pub const fn attempt_id(&self) -> u64 {
self.attempt_id
}
pub const fn provider_request_id(&self) -> u64 {
self.provider_request_id
}
pub const fn exclusive_token(&self) -> u64 {
self.exclusive_token
}
pub const fn is_authority(&self) -> bool {
false
}
pub const fn consumed_any_input(&self) -> bool {
false
}
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS412ExclusionGatedJoinPreflightOutcome {
AwaitingAdmission,
AwaitingInputs {
authorities_ready: bool,
delivery_receipt_ready: bool,
},
Backpressured,
Ready(G8lS412ExclusionGatedJoinPreflightReceipt),
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS412ExclusionGatedJoinPreflightError {
WrongCpu,
AdmissionBindingDrift,
GateTokenMismatch,
S411(G8lS411EphemeralExclusionAdmissionError),
#[cfg(all(target_arch = "aarch64", target_os = "none", feature = "board-rpi5"))]
S242(crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s179_execution_caller_notification_sgi_sender_runtime_callsite_request::G8lS242SenderRuntimeCallsiteStateError),
#[cfg(all(target_arch = "aarch64", target_os = "none", feature = "board-rpi5"))]
S240(crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s179_execution_caller_notification_sgi_delivery::G8lS240ReceiptPendingError),
#[cfg(all(target_arch = "aarch64", target_os = "none", feature = "board-rpi5"))]
S243(crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s242_authority_return_s240_receipt_deferred_consumer::G8lS243DeferredStateError),
}
fn admission_is_exact(admission: G8lS411EphemeralExclusionAdmissionView) -> bool {
admission.attempt_id != 0
&& admission.provider_request_id != 0
&& admission.exclusive_token != 0
&& admission.live_gate_matched_at_construction
&& admission.requires_live_gate_match_at_consumption
&& !admission.is_standalone_authority
}
pub fn preflight_s412_exclusion_gated_join(
admission: Option<G8lS411EphemeralExclusionAdmissionView>,
caller_cpu: usize,
active_exclusive_token: Option<u64>,
authorities_ready: bool,
delivery_receipt_ready: bool,
output_free: bool,
) -> Result<G8lS412ExclusionGatedJoinPreflightOutcome, G8lS412ExclusionGatedJoinPreflightError> {
if caller_cpu != 0 {
return Err(G8lS412ExclusionGatedJoinPreflightError::WrongCpu);
}
let Some(admission) = admission else {
return Ok(G8lS412ExclusionGatedJoinPreflightOutcome::AwaitingAdmission);
};
if !admission_is_exact(admission) {
return Err(G8lS412ExclusionGatedJoinPreflightError::AdmissionBindingDrift);
}
if active_exclusive_token != Some(admission.exclusive_token) {
return Err(G8lS412ExclusionGatedJoinPreflightError::GateTokenMismatch);
}
if !output_free {
return Ok(G8lS412ExclusionGatedJoinPreflightOutcome::Backpressured);
}
if !authorities_ready || !delivery_receipt_ready {
return Ok(G8lS412ExclusionGatedJoinPreflightOutcome::AwaitingInputs {
authorities_ready,
delivery_receipt_ready,
});
}
Ok(G8lS412ExclusionGatedJoinPreflightOutcome::Ready(
G8lS412ExclusionGatedJoinPreflightReceipt {
attempt_id: admission.attempt_id,
provider_request_id: admission.provider_request_id,
exclusive_token: admission.exclusive_token,
},
))
}
#[cfg(all(target_arch = "aarch64", target_os = "none", feature = "board-rpi5"))]
pub fn service_s412_exclusion_gated_join_preflight_on_cpu0(
) -> Result<G8lS412ExclusionGatedJoinPreflightOutcome, G8lS412ExclusionGatedJoinPreflightError> {
use crate::g8l_runtime_contract::CPU0;
if crate::percpu::try_current_cpu_id() != Some(CPU0) {
return Err(G8lS412ExclusionGatedJoinPreflightError::WrongCpu);
}
let admission = crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s411_ephemeral_exclusion_admission_constructor::inspect_s411_ephemeral_exclusion_admission_on_cpu0()
.map_err(G8lS412ExclusionGatedJoinPreflightError::S411)?;
let active_token = crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s246_whole_scheduler_read_access_guard::S247_PRODUCTION_WHOLE_SCHEDULER_ACCESS_GATE
.active_exclusive_token();
let authorities_ready = crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s179_execution_caller_notification_sgi_sender_runtime_callsite_request::s242_returned_runtime_authorities_pending_on_cpu0()
.map_err(G8lS412ExclusionGatedJoinPreflightError::S242)?;
let delivery_receipt_ready = crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s179_execution_caller_notification_sgi_delivery::s240_sgi_delivery_receipt_pending_on_cpu0()
.map_err(G8lS412ExclusionGatedJoinPreflightError::S240)?;
let output_free = !crate::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s242_authority_return_s240_receipt_deferred_consumer::s243_deferred_s187_handoff_pending_on_cpu0()
.map_err(G8lS412ExclusionGatedJoinPreflightError::S243)?;
preflight_s412_exclusion_gated_join(
admission,
CPU0,
active_token,
authorities_ready,
delivery_receipt_ready,
output_free,
)
}
snippet sha256: 177c54dcf632…file sha256: 177c54dcf632…
02 · Doğrulayan test kodu
Operations komutuna bağlı focused test
tam dosyaL1–L123
simulation/tests/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight.rs::S412 exclusion gated join preflight focused tests
use aselsan_microkernel_simulation::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s411_ephemeral_exclusion_admission_constructor::G8lS411EphemeralExclusionAdmissionView;
use aselsan_microkernel_simulation::g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight::*;
fn admission() -> G8lS411EphemeralExclusionAdmissionView {
G8lS411EphemeralExclusionAdmissionView {
attempt_id: 7,
provider_request_id: 8,
exclusive_token: 9,
live_gate_matched_at_construction: true,
requires_live_gate_match_at_consumption: true,
is_standalone_authority: false,
}
}
#[test]
fn constants_keep_s412_non_consuming() {
assert_eq!(S412_PRODUCTION_PREFLIGHT_CALLSITES, 1);
assert_eq!(S412_LINEAR_INPUT_TAKE_SITES, 0);
assert_eq!(S412_PRODUCTION_S243_JOIN_CALLSITES, 0);
assert!(S412_FOUR_WAY_READINESS_PREFLIGHT_COMPLETE);
assert!(!S412_END_TO_END_EXCLUSION_ADMISSION_COMPLETE);
}
#[test]
fn all_exact_inputs_produce_non_authoritative_ready_receipt() {
let outcome =
preflight_s412_exclusion_gated_join(Some(admission()), 0, Some(9), true, true, true)
.unwrap();
let G8lS412ExclusionGatedJoinPreflightOutcome::Ready(receipt) = outcome else {
panic!("all exact inputs must be ready")
};
assert_eq!(receipt.attempt_id(), 7);
assert_eq!(receipt.provider_request_id(), 8);
assert_eq!(receipt.exclusive_token(), 9);
assert!(!receipt.is_authority());
assert!(!receipt.consumed_any_input());
}
#[test]
fn absent_admission_waits_without_error() {
assert_eq!(
preflight_s412_exclusion_gated_join(None, 0, None, true, true, true),
Ok(G8lS412ExclusionGatedJoinPreflightOutcome::AwaitingAdmission)
);
}
#[test]
fn stale_gate_token_fails_closed() {
assert_eq!(
preflight_s412_exclusion_gated_join(Some(admission()), 0, Some(10), true, true, true),
Err(G8lS412ExclusionGatedJoinPreflightError::GateTokenMismatch)
);
}
#[test]
fn occupied_output_backpressures_before_input_readiness() {
assert_eq!(
preflight_s412_exclusion_gated_join(Some(admission()), 0, Some(9), false, false, false),
Ok(G8lS412ExclusionGatedJoinPreflightOutcome::Backpressured)
);
}
#[test]
fn partial_inputs_are_reported_exactly() {
assert_eq!(
preflight_s412_exclusion_gated_join(Some(admission()), 0, Some(9), true, false, true),
Ok(G8lS412ExclusionGatedJoinPreflightOutcome::AwaitingInputs {
authorities_ready: true,
delivery_receipt_ready: false,
})
);
}
#[test]
fn wrong_cpu_is_rejected_first() {
assert_eq!(
preflight_s412_exclusion_gated_join(Some(admission()), 1, Some(9), true, true, true),
Err(G8lS412ExclusionGatedJoinPreflightError::WrongCpu)
);
}
#[test]
fn production_preflight_reads_each_real_pending_surface_without_take() {
let source = include_str!("../../kernel/src/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight.rs");
let start = source
.find("service_s412_exclusion_gated_join_preflight_on_cpu0")
.unwrap();
let body = &source[start..];
for required in [
"inspect_s411_ephemeral_exclusion_admission_on_cpu0",
"active_exclusive_token",
"s242_returned_runtime_authorities_pending_on_cpu0",
"s240_sgi_delivery_receipt_pending_on_cpu0",
"s243_deferred_s187_handoff_pending_on_cpu0",
] {
assert!(
body.contains(required),
"missing readiness surface: {required}"
);
}
for forbidden in [
"take_s411_",
"take_s242_",
"take_sgi_receipt_and_consume_s179_on_cpu0",
] {
assert!(
!body.contains(forbidden),
"preflight consumed input: {forbidden}"
);
}
}
#[test]
fn s412_is_separately_registered_and_wired_after_s411() {
let name = "g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight";
let main = include_str!("../../kernel/src/main.rs");
let sim = include_str!("../src/lib.rs");
assert!(main.contains(&format!("mod {name};")));
assert!(sim.contains(&format!("pub mod {name};")));
let successor = include_str!("../../kernel/src/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s413_exclusion_gated_s243_join.rs");
assert!(successor.contains("service_s412_exclusion_gated_join_preflight_on_cpu0"));
}
snippet sha256: 02dd65fc6442…file sha256: 02dd65fc6442…
03 · Kapı kimlik kaydı
Operations sıra, kimlik ve başlık bağı
tam Operations kaydıL287–L303
website/src/lib/operations.ts::g8l-s412-exclusion-gated-join-preflight-partial
{
id: "g8l-s412-exclusion-gated-join-preflight-partial",
sequence: 412,
slug: "exclusion_gated_join_preflight",
title: "Exclusion-gated join preflight",
focusedTests: 9,
sourceBytes: 7414,
sourceSha256:
"177c54dcf6328ea5a2e12bffa8743c549cc42fe8d779a4c0e0c11e49e7c8a206",
testBytes: 4652,
testSha256:
"02dd65fc6442b89fdd6c594256f155d2710f1cb8ff84d8de3f0e1d68aeba6b9a",
acceptance:
"S411 admission, S243 readiness, S240 receipt ve handoff-slot uygunluğu dört-yollu non-consuming typed preflight'te birleştirilir.",
retainedBoundary:
"Linear input take ve production S243 join çağrısı bu kapıda sıfırdır.",
},snippet sha256: a3b437c72987…file sha256: 9726dbf00f84…
Focused test komutu
CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s412_exclusion_gated_join_preflight -- --test-threads=1proof: docs/M8.1-RPi5-G8l-S412-Exclusion-Gated-Join-Preflight-Proof.md
Registry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06