ASELSANMicrokernel
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: 177c54dcf632file 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: 02dd65fc6442file 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: a3b437c72987file 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=1
proof: 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