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: c60794da1b29…file 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: d56f06caecdc…file sha256: 9726dbf00f84…
Kayıtlı yürütme/kanıt komutu
freeze CPU1-only task, stack, frame, timer-epoch and bounded stage invariantsRegistry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9