ASELSANMicrokernel
S94 · SOURCE-BOUND GATE EVIDENCE

G8h contract/parser GREEN; S95 dormant runtime sırada

Operations komutu/kapı ailesi → gerçek repository yürütme sözleşmesi Bu sayfa yalnız S94 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S94Komut / fiziksel sözleşmeOperations id exactsource SHA exact

operation: rpi5-g8h-contract-parser-runtime-stop

script/Makefile/config · Operations · 2 exact excerpt

sequence-bound=true · implementation-bound=false
01 · Yürütme sözleşmesi

Gerçek script / Makefile / config kaynağı

tam Rust öğesiL1379–L1764
kernel/src/rpi5_g8h.rs::rpi5_g8h_try_handle_secondary_irq

/// Handle one CPU1-owned PPI27 and return the exact frame that exceptions.S
/// must restore. `None` means not owned; `Some(ctx)` means handled without a
/// switch; `Some(other)` is an EOI-complete task redirect.
#[no_mangle]
#[inline(never)]
pub fn rpi5_g8h_try_handle_secondary_irq(
    ctx: &mut ExceptionContext,
    ack: u32,
    int_id: u32,
) -> Option<*mut ExceptionContext> {
    if !rpi5_g8h_secondary_irq_active() {
        return None;
    }
    let ctx_ptr = ctx as *mut ExceptionContext;
    let tpidr = read_tpidr();
    if tpidr != TARGET_CPU_INDEX {
        return consume_owned_irq_error(ctx, ack, int_id, ERR_TPIDR, TARGET_CPU_INDEX, tpidr);
    }
    let ack_intid = gic::interrupt_id(ack);
    if int_id != ack_intid {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_ACK_RAW,
            int_id as u64,
            ack_intid as u64,
        );
    }
    if int_id != TIMER_PPI {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_IRQ_ID,
            TIMER_PPI as u64,
            int_id as u64,
        );
    }
    if ack != TIMER_PPI {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_ACK_RAW,
            TIMER_PPI as u64,
            ack as u64,
        );
    }
    if ctx.spsr_el1 & SPSR_IRQ_MASK != 0
        || ctx.spsr_el1 & SPSR_DAF_MASK != SPSR_DAF_MASK
        || ctx.spsr_el1 & SPSR_MODE_MASK != SPSR_EL1H_MODE
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_DAIF,
            SPSR_EL1H_IRQ_UNMASKED,
            ctx.spsr_el1,
        );
    }

    let prior_switches = SWITCHES.load(Ordering::Acquire);
    let expected_stage = match stage_for_switches(prior_switches) {
        Some(value) if value != STAGE_SWITCH4 => value,
        _ => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_IRQ_STAGE,
                STAGE_SWITCH4,
                STAGE.load(Ordering::Relaxed),
            )
        }
    };
    let stage = STAGE.load(Ordering::Acquire);
    if stage != expected_stage {
        return consume_owned_irq_error(ctx, ack, int_id, ERR_IRQ_STAGE, expected_stage, stage);
    }
    let current = CURRENT.load(Ordering::Acquire);
    let expected_current = if prior_switches & 1 == 0 {
        TASK_A
    } else {
        TASK_B
    };
    if current != expected_current
        || !frame_in_stack(
            ctx_ptr as u64,
            task_stack_bounds(current).0 as u64,
            task_stack_bounds(current).1 as u64,
        )
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_FRAME_OWNER,
            expected_current,
            ctx_ptr as u64,
        );
    }
    if current == TASK_A
        && (ctx_ptr as u64).checked_add(TRAP_FRAME_BYTES as u64)
            != Some(TASK_A_ENTRY_SP.load(Ordering::Acquire))
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_FRAME_STABILITY,
            TASK_A_ENTRY_SP.load(Ordering::Relaxed),
            ctx_ptr as u64,
        );
    }

    let expected_prior = IRQ_DELIVERIES.load(Ordering::Acquire);
    if expected_prior >= EXPECTED_CPU1_DELIVERIES
        || IRQ_ACKS.load(Ordering::Acquire) != expected_prior
        || IRQ_EOIS.load(Ordering::Acquire) != expected_prior
        || DEADLINE_ADVANCES.load(Ordering::Acquire) != expected_prior
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_IRQ_COUNTS,
            expected_prior,
            IRQ_ACKS.load(Ordering::Relaxed),
        );
    }
    let delivery = match expected_prior.checked_add(1) {
        Some(value) => value,
        None => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_TIMER_ARITHMETIC,
                expected_prior,
                1,
            )
        }
    };
    let before = match timer::rpi5_g8g_periodic_snapshot(SLOT_CPU1) {
        Ok(snapshot) => snapshot,
        Err(_) => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_TIMER_SNAPSHOT,
                SLOT_CPU1 as u64,
                0,
            )
        }
    };
    let expected_current_cval = match expected_deadline(before.start_count, before.period, delivery)
    {
        Some(value) => value,
        None => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_TIMER_ARITHMETIC,
                before.start_count,
                delivery,
            )
        }
    };
    let next_delivery = match delivery.checked_add(1) {
        Some(value) => value,
        None => {
            return consume_owned_irq_error(ctx, ack, int_id, ERR_TIMER_ARITHMETIC, delivery, 1)
        }
    };
    let expected_next = match expected_deadline(before.start_count, before.period, next_delivery) {
        Some(value) => value,
        None => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_TIMER_ARITHMETIC,
                before.start_count,
                next_delivery,
            )
        }
    };
    let fired_count = timer::read_count();
    if before.ticks != expected_prior
        || before.next_cval != expected_current_cval
        || fired_count < before.next_cval
        || fired_count >= expected_next
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_CVAL,
            expected_current_cval,
            before.next_cval,
        );
    }
    let drift = match fired_count.checked_sub(before.next_cval) {
        Some(value) => value,
        None => {
            return consume_owned_irq_error(
                ctx,
                ack,
                int_id,
                ERR_TIMER_ARITHMETIC,
                before.next_cval,
                fired_count,
            )
        }
    };
    let after = match timer::rpi5_g8g_advance_local_periodic(SLOT_CPU1) {
        Ok(snapshot) => snapshot,
        Err(_) => {
            return consume_owned_irq_error(ctx, ack, int_id, ERR_TIMER_ADVANCE, expected_next, 0)
        }
    };
    if after.start_count != before.start_count
        || after.period != before.period
        || after.next_cval != expected_next
        || after.ticks != delivery
    {
        return consume_owned_irq_error(
            ctx,
            ack,
            int_id,
            ERR_TIMER_ADVANCE,
            expected_next,
            after.next_cval,
        );
    }
    let final_ctl = if delivery == EXPECTED_CPU1_DELIVERIES {
        match timer::rpi5_g8g_disable_local_timer(SLOT_CPU1) {
            Ok(control) => control,
            Err(_) => return consume_owned_irq_error(ctx, ack, int_id, ERR_TIMER_DISABLE, 0b10, 0),
        }
    } else {
        0
    };

    gic::end_of_interrupt(ack);
    completion_barrier();
    if let Err(code) = store_outgoing_frame(current, ctx_ptr) {
        return fail_owned_after_eoi(ctx, code, target_frame_for(current), ctx_ptr as u64);
    }
    IRQ_DELIVERIES.store(delivery, Ordering::Relaxed);
    IRQ_ACKS.store(delivery, Ordering::Relaxed);
    IRQ_EOIS.store(delivery, Ordering::Relaxed);
    DEADLINE_ADVANCES.store(delivery, Ordering::Relaxed);

    let is_switch_delivery = delivery == EXPECTED_SWITCH_LOCAL_TICKS[0]
        || delivery == EXPECTED_SWITCH_LOCAL_TICKS[1]
        || delivery == EXPECTED_SWITCH_LOCAL_TICKS[2]
        || delivery == EXPECTED_SWITCH_LOCAL_TICKS[3];
    if !is_switch_delivery {
        return Some(ctx_ptr);
    }
    let switch_index = prior_switches as usize;
    if switch_index >= REQUIRED_SWITCHES as usize
        || EXPECTED_SWITCH_LOCAL_TICKS[switch_index] != delivery
    {
        return fail_owned_after_eoi(ctx, ERR_SWITCH_ORDER, prior_switches, delivery);
    }
    let progress_sample = TASK_PROGRESS.load(Ordering::Acquire);
    let (expected_progress, expected_a_segments, expected_b_segments) = match switch_index {
        0 => (TASK_PROGRESS_A1, TASK_SEGMENT_ONE, 0),
        1 => (TASK_PROGRESS_B1, TASK_SEGMENT_ONE, TASK_SEGMENT_ONE),
        2 => (TASK_PROGRESS_A2, TASK_SEGMENT_TWO, TASK_SEGMENT_ONE),
        3 => (TASK_PROGRESS_B2, TASK_SEGMENT_TWO, TASK_SEGMENT_TWO),
        _ => return fail_owned_after_eoi(ctx, ERR_SWITCH_ORDER, 3, switch_index as u64),
    };
    if progress_sample != expected_progress
        || TASK_A_RUN_SEGMENTS.load(Ordering::Acquire) != expected_a_segments
        || TASK_B_RUN_SEGMENTS.load(Ordering::Acquire) != expected_b_segments
    {
        return fail_owned_after_eoi(ctx, ERR_PROGRESS, expected_progress, progress_sample);
    }

    let next = if current == TASK_A { TASK_B } else { TASK_A };
    let target_frame = target_frame_for(next);
    if !task_frame_contains(next, target_frame) {
        return fail_owned_after_eoi(ctx, ERR_TARGET_FRAME, next, target_frame);
    }
    let target = target_frame as *mut ExceptionContext;
    let target_spsr = unsafe { (*target).spsr_el1 };
    if target_spsr & SPSR_TASK_MASK != SPSR_EL1H_IRQ_UNMASKED {
        return fail_owned_after_eoi(ctx, ERR_DAIF, SPSR_EL1H_IRQ_UNMASKED, target_spsr);
    }
    if delivery == EXPECTED_CPU1_DELIVERIES {
        unsafe {
            (*target).spsr_el1 |= SPSR_IRQ_MASK;
        }
        if IRQ_HANDLER_ACTIVE
            .compare_exchange(true, false, Ordering::AcqRel, Ordering::Acquire)
            .is_err()
        {
            return fail_owned_after_eoi(ctx, ERR_IRQ_OWNERSHIP, 1, 0);
        }
    }

    let next_switch = match prior_switches.checked_add(1) {
        Some(value) => value,
        None => return fail_owned_after_eoi(ctx, ERR_TIMER_ARITHMETIC, prior_switches, 1),
    };
    let next_stage = match stage_for_switches(next_switch) {
        Some(value) => value,
        None => return fail_owned_after_eoi(ctx, ERR_SWITCH_ORDER, REQUIRED_SWITCHES, next_switch),
    };
    let evidence_progress = progress_sample;
    SWITCH_TICKS[switch_index].store(delivery, Ordering::Relaxed);
    SWITCH_ACK_RAW[switch_index].store(ack as u64, Ordering::Relaxed);
    SWITCH_EOI_RAW[switch_index].store(ack as u64, Ordering::Relaxed);
    SWITCH_PREV_CVAL[switch_index].store(before.next_cval, Ordering::Relaxed);
    SWITCH_NEXT_CVAL[switch_index].store(after.next_cval, Ordering::Relaxed);
    SWITCH_FIRED_COUNT[switch_index].store(fired_count, Ordering::Relaxed);
    SWITCH_DRIFT_COUNTS[switch_index].store(drift, Ordering::Relaxed);
    SWITCH_FROM_FRAME[switch_index].store(ctx_ptr as u64, Ordering::Relaxed);
    SWITCH_TO_FRAME[switch_index].store(target_frame, Ordering::Relaxed);
    SWITCH_PROGRESS[switch_index].store(evidence_progress, Ordering::Relaxed);
    SWITCH_PROGRESS_SAMPLE[switch_index].store(progress_sample, Ordering::Relaxed);
    if CURRENT
        .compare_exchange(current, next, Ordering::AcqRel, Ordering::Acquire)
        .is_err()
        || SWITCHES
            .compare_exchange(
                prior_switches,
                next_switch,
                Ordering::AcqRel,
                Ordering::Acquire,
            )
            .is_err()
    {
        return fail_owned_after_eoi(
            ctx,
            ERR_SWITCH_ORDER,
            current,
            CURRENT.load(Ordering::Relaxed),
        );
    }
    if delivery == EXPECTED_CPU1_DELIVERIES {
        FINAL_TIMER_CTL.store(final_ctl, Ordering::Relaxed);
        DISABLED_NEXT_CVAL.store(after.next_cval, Ordering::Relaxed);
        if COMPLETION_TOKEN
            .compare_exchange(
                COMPLETION_EMPTY,
                COMPLETION_READY,
                Ordering::AcqRel,
                Ordering::Acquire,
            )
            .is_err()
        {
            return fail_owned_after_eoi(
                ctx,
                ERR_COMPLETION,
                COMPLETION_EMPTY,
                COMPLETION_TOKEN.load(Ordering::Relaxed),
            );
        }
    }
    if STAGE
        .compare_exchange(
            expected_stage,
            next_stage,
            Ordering::Release,
            Ordering::Acquire,
        )
        .is_err()
    {
        return fail_owned_after_eoi(
            ctx,
            ERR_IRQ_STAGE,
            expected_stage,
            STAGE.load(Ordering::Relaxed),
        );
    }
    Some(target_frame as *mut ExceptionContext)
}
snippet sha256: c60794da1b29file sha256: 624b78efcdd3
02 · Kapı kimlik kaydı

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

tam Operations kaydıL28468–L28557
website/src/lib/operations.ts::rpi5-g8h-contract-parser-runtime-stop
  {
    id: "rpi5-g8h-contract-parser-runtime-stop",
    date: "2026-08-22",
    sequence: 94,
    status: "partial",
    title: "G8h contract/parser GREEN; S95 dormant runtime sırada",
    summary:
      "Sequence 93 ile kalıcılaşan physical BOOT8G prerequisite'i değiştirilmeden G8h'nin ilk host-only kapısı açıldı. Allocation-free contract ve strict parser, yalnız CPU1/MPIDR 0x100/PPI27 üzerinde iki ayrı statik 64 KiB EL1 stack arasında exact ABABA local preemption sözleşmesini dondurur. Yeni timer epoch'i G8g'nin off+masked final durumundan başlar; ilk task doğrudan kendi stack'inde çalışır, switch'ler local tick 10/20/30/40'ta gerçekleşir ve 40 delivery/ack/EOI/deadline-advance sonrası timer yeniden off+masked olur. Frame/stack alias, eksik EOI, deadline sapması, CPU0 state mutasyonu, GIC pending/active kalıntısı ve generic iş fail-closed reddedilir. Canonical CLI yalnız `source=synthetic physical=NO` PASS'tir. `rpi5_g8h.rs`, production wiring, layout, image/package, microSD, UART capture, power-on ve fiziksel BOOT8H yoktur; Pi kapalı tutulur. S94 contract/parser GREEN, aktif sonraki tek kapı S95 dormant bounded runtime source TDD'dir.",
    evidence: [
      "Immutable prerequisite: S92 18.978 B / 4abf8bb1…1a2 physical BOOT8G raw ve S93 9-file permanent archive değişmedi; son fiziksel PASS S92 BOOT8G'dir.",
      "Allocation-free G8h contract: target CPU1, MPIDR=0x100, TPIDR=1, PPI27/timer-slot1, new timer epoch ve prior timer OFF/IMASK ON.",
      "Exact local schedule: iki static 64 KiB stack, no-alias, ABABA, quantum 10 ve switch local ticks 10/20/30/40.",
      "Exact bounded totals: 40 CPU1 IRQ/delivery/ack/EOI/deadline advance/local tick; direct dispatch 1, dispatcher IRQ dispatch 0 ve return IRQ 0.",
      "Integer context GPR31+ELR+SPSR+SP=264 B; saved frame 272 B/16-byte aligned; stack 4 KiB aligned ve iki-word canary ile korunur; FP/SIMD trap'te kalır.",
      "Dördüncü IRQ B'den A'ya redirect eder; B normal return yapmaz, A completion token'la monitor stack'e döner ve SP exact restore edilir.",
      "Post-stop owner CPU1; post-stop IRQ yok, final timer OFF/IMASK ON, GIC enabled=1 ve pending/active=0; CPU0 next-CVAL/ticks immutable ve state mutation=0.",
      "Strict parser full G8→G8h prerequisite zincirini, marker/field count-order-set kurallarını, binary framing'i, checked deadline kronolojisini ve stack/frame ownership'i fail-closed bağlar.",
      "BOOT8G marker'ı G8H0'a immediately adjacent; G8h block exact altı canonical single-space satır, LF/CRLF kabulü ve BOOT8H terminal EOF kuralıyla dondurulur.",
      "Stage timeout MAX_STAGE_PERIODS=200; monitor SP nonzero/aligned ve iki task stack'inin dışında, post-stop check ise disabled deadline'dan erken olmayan ama bir period'dan kısa bounded pencerededir.",
      "`make verify-rpi5-g8h-contract` host-only contract/source/parser regresyonlarını ve CLI example check'ini PASS verdi.",
      "Final target exact 24/24 PASS: historical G8g UART 11/11 + G8h source 5/5 + G8h UART/adversarial 8/8; CLI example check PASS. Final release 13/13 PASS (G8h source+UART) ve release canonical CLI PASS.",
      "Adversarial matrix 301/301 fail-closed rejection: 213 every-field mutation + 88 targeted boundary; bağımsız trailing/gap/whitespace/SP/stack/timing PoC'leri 9/9 exit 1.",
      "Contract exact 6.318 B / b07445fba49bf78a402128a5435606dad4450e370cf84718ae16fb9962b42f99; strict parser 49.347 B / fea779511d237781d1cb9d671fb39787f6a0fd21e6ad07904c30cced2e9fb8c1.",
      "Canonical suffix exact 3.499 B / 03b484ffe8db0db007ab733634c57228909760365a5a6ce85e5515666b71172d; source test 9.201 B / e964ad6628ae811b3da20ca1b5bf742fcd427e9c6c331dc703990f6c93822921.",
      "UART test exact 21.325 B / 574d932ee2567681f7f7bfab619ed8bb056c70ed821a0650eb311edc56e8b614; CLI 2.537 B / 8714753f86e5589409f824093fdcfbd23eda7cb4aea59a516a8a4885e23c8179.",
      "Registrations: simulation/src/lib.rs 1.573 B / 4cdf0ce19eda2a1dd21c778ea4922f74ae97b820e413f8a85f222f01227df2b8; Makefile 24.244 B / 6628ab5630805364a79f9f971a015d27186b6dc7289decf9f40b7842dd1fc6b8.",
      "Frozen eight-entry identity-list composite SHA-256 e8fa44c66ed3145edd4bed0f262d3a40d86f15050ff8a07f4d9166daa07aef5d.",
      "S94 proof exact 233 satır / 9.197 B / b57115c5f4f2059da1ebbc66945a98dedfaa76224a47a3fa2d0816cc69754a28.",
      "Canonical CLI PASS: `source=synthetic physical=NO`, order ABABA, switch ticks 10/20/30/40 ve scope CPU1_LOCAL_STATIC_PREEMPTION_ONLY.",
      "S94 STOP audit: G8h runtime dosyası, main/exception/timer production reachability, runtime/layout/package hedefi ve BOOT8H physical artifact yok.",
      "Kullanıcı Pi'nin kapatıldığını teyit etti; S94 hiçbir aygıt, kart, UART descriptor, power veya physical raw işlemi yapmadı.",
    ],
    terminalSessionsNote:
      "Sequence 94 oturumları host-only contract/parser ve fail-closed absence denetimidir; sentetik fixture fiziksel UART kanıtı değildir.",
    terminalSessions: [
      {
        id: "g8h-sequence94-contract-source",
        title: "Allocation-free local static-preemption sözleşmesi",
        commandLines: [
          "freeze CPU1-only task, stack, frame, timer-epoch and bounded stage invariants",
          "run G8h source tests and historical G8g parser regression",
        ],
        outputLines: [
          "target=CPU1 MPIDR=0x100 PPI27 slot1 · tasks=2 stacks=2x64K",
          "order=ABABA · quantum=10 · switch_ticks=10/20/30/40",
          "allocation/alias/fallback surfaces=REJECT",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
      {
        id: "g8h-sequence94-strict-parser",
        title: "Strict sentetik validator ve adversarial sınır",
        commandLines: [
          "make verify-rpi5-g8h-contract",
          "cargo run -p aselsan_microkernel_simulation --example verify_rpi5_g8h_log -- --canonical",
        ],
        outputLines: [
          "aggregate=24/24 PASS · release G8h=13/13 PASS · CLI checks=PASS",
          "adversarial=301/301 rejected · every-field=213 · independent PoC=9/9 exit1",
          "synthetic CLI=PASS physical=NO · scope=CPU1_LOCAL_STATIC_PREEMPTION_ONLY",
          "delivery/ack/eoi/advance/local_ticks=40/40/40/40/40 · final=off+masked",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
      {
        id: "g8h-sequence94-runtime-stop",
        title: "Production reachability ve fiziksel artefakt STOP denetimi",
        commandLines: [
          "verify rpi5_g8h runtime source and production references are absent",
          "verify runtime/layout/package/device/UART/power/BOOT8H gates remain unopened",
        ],
        outputLines: [
          "runtime_source=ABSENT · production_reachability=ABSENT",
          "image/package/microSD/UART/power/BOOT8H=NOT_PERFORMED",
          "S94=GREEN · next=S95_DORMANT_BOUNDED_RUNTIME",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
    ],
    limitations: [
      "S94 yalnız allocation-free contract, canonical sentetik fixture ve strict host parser kabulüdür; fiziksel BOOT8H değildir.",
      "`kernel/src/rpi5_g8h.rs` yoktur ve production main/exception/timer akışında G8h erişimi bulunmaz; S95 dormant bounded runtime ayrı kapıdır.",
      "Image/package, reproducibility, microSD write, UART arm/capture, power-on, raw/archive ve promotion kapıları STOP'tur.",
      "Generic SMP scheduler/runqueue, migration, load balancing, ASID/TLB shootdown, CPU2/CPU3, hotplug ve soak kapalıdır.",
      "Production deployment dirty/untracked workspace ve stale 47d22c9 source etiketiyle yapılır; canlı artifact doğrulansa da Git-provider provenance kurulmuş sayılmaz.",
    ],
  },
snippet sha256: d56f06caecdcfile sha256: 9726dbf00f84
Kayıtlı yürütme/kanıt komutu
freeze CPU1-only task, stack, frame, timer-epoch and bounded stage invariants
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06