S83 · SOURCE-BOUND GATE EVIDENCE
G8g counter sözleşmesi fiziksel CNTVCT nedenselliğiyle düzeltildi
Operations komutu/kapı ailesi → gerçek repository yürütme sözleşmesi Bu sayfa yalnız S83 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.
S83Komut / fiziksel sözleşmeOperations id exactsource SHA exact
operation: rpi5-g8g-counter-contract-corrected
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 öğesiL500–L641
kernel/src/rpi5_g8g.rs::rpi5_g8g_try_handle_secondary_irq
/// Consume exactly two CPU1-local PPI27 interrupts while ownership is active.
#[no_mangle]
#[inline(never)]
pub fn rpi5_g8g_try_handle_secondary_irq(
ctx: &mut ExceptionContext,
ack: u32,
int_id: u32,
) -> bool {
if !rpi5_g8g_secondary_irq_active() {
return false;
}
let stage = STAGE.load(Ordering::Acquire);
if stage != STAGE_ARMED && stage != STAGE_IRQ1 {
return consume_irq_error(ctx, ack, int_id, ERR_THIRD_IRQ, STAGE_IRQ2, stage);
}
if int_id != TIMER_PPI {
return consume_irq_error(
ctx,
ack,
int_id,
ERR_IRQ_ID,
TIMER_PPI as u64,
int_id as u64,
);
}
if ack != TIMER_PPI {
return consume_irq_error(ctx, ack, int_id, ERR_ACK_RAW, TIMER_PPI as u64, ack as u64);
}
if ctx.spsr_el1 & SPSR_IRQ_MASK != 0 {
return consume_irq_error(ctx, ack, int_id, ERR_FINAL_DAIF, 0, ctx.spsr_el1);
}
let expected_prior = if stage == STAGE_ARMED { 0 } else { 1 };
if IRQ_DELIVERIES.load(Ordering::Acquire) != expected_prior
|| IRQ_ACKS.load(Ordering::Acquire) != expected_prior
|| IRQ_EOIS.load(Ordering::Acquire) != expected_prior
|| DEADLINE_ADVANCES.load(Ordering::Acquire) != expected_prior
{
return consume_irq_error(
ctx,
ack,
int_id,
ERR_IRQ_COUNTS,
expected_prior,
IRQ_DELIVERIES.load(Ordering::Relaxed),
);
}
let before = match timer::rpi5_g8g_periodic_snapshot(SLOT_CPU1) {
Ok(snapshot) => snapshot,
Err(_) => return consume_irq_error(ctx, ack, int_id, ERR_TIMER_SNAPSHOT, 1, 0),
};
let fired_count = timer::read_count();
let after = match timer::rpi5_g8g_advance_local_periodic(SLOT_CPU1) {
Ok(snapshot) => snapshot,
Err(_) => return consume_irq_error(ctx, ack, int_id, ERR_TIMER_ADVANCE, 1, 0),
};
let expected_next = match before.next_cval.checked_add(before.period) {
Some(value) => value,
None => {
return consume_irq_error(
ctx,
ack,
int_id,
ERR_TIMER_ARITHMETIC,
before.next_cval,
before.period,
)
}
};
let expected_tick = match before.ticks.checked_add(1) {
Some(value) => value,
None => return consume_irq_error(ctx, ack, int_id, ERR_TIMER_ARITHMETIC, before.ticks, 1),
};
if after.next_cval != expected_next
|| after.ticks != expected_tick
|| fired_count < before.next_cval
|| fired_count >= after.next_cval
{
return consume_irq_error(
ctx,
ack,
int_id,
ERR_TIMER_ARITHMETIC,
expected_next,
after.next_cval,
);
}
let drift = fired_count - before.next_cval;
let delivery = expected_prior + 1;
let final_ctl = if delivery == EXPECTED_CPU1_DELIVERIES {
match timer::rpi5_g8g_disable_local_timer(SLOT_CPU1) {
Ok(control) => control,
Err(_) => return consume_irq_error(ctx, ack, int_id, ERR_TIMER_DISABLE, 0b10, 0),
}
} else {
0
};
gic::end_of_interrupt(ack);
completion_barrier();
IRQ_DELIVERIES.store(delivery, Ordering::Relaxed);
IRQ_ACKS.store(delivery, Ordering::Relaxed);
IRQ_EOIS.store(delivery, Ordering::Relaxed);
DEADLINE_ADVANCES.store(delivery, Ordering::Relaxed);
if delivery == 1 {
IRQ1_ACK_RAW.store(ack as u64, Ordering::Relaxed);
IRQ1_EOI_RAW.store(ack as u64, Ordering::Relaxed);
IRQ1_PREV_CVAL.store(before.next_cval, Ordering::Relaxed);
IRQ1_NEXT_CVAL.store(after.next_cval, Ordering::Relaxed);
IRQ1_FIRED_COUNT.store(fired_count, Ordering::Relaxed);
IRQ1_DRIFT_COUNTS.store(drift, Ordering::Relaxed);
IRQ1_LOCAL_TICK.store(after.ticks, Ordering::Relaxed);
ctx.spsr_el1 &= !SPSR_IRQ_MASK;
} else {
IRQ2_ACK_RAW.store(ack as u64, Ordering::Relaxed);
IRQ2_EOI_RAW.store(ack as u64, Ordering::Relaxed);
IRQ2_PREV_CVAL.store(before.next_cval, Ordering::Relaxed);
IRQ2_NEXT_CVAL.store(after.next_cval, Ordering::Relaxed);
IRQ2_FIRED_COUNT.store(fired_count, Ordering::Relaxed);
IRQ2_DRIFT_COUNTS.store(drift, Ordering::Relaxed);
IRQ2_LOCAL_TICK.store(after.ticks, Ordering::Relaxed);
FINAL_TIMER_CTL.store(final_ctl, Ordering::Relaxed);
ctx.spsr_el1 |= SPSR_IRQ_MASK;
}
let next_stage = if delivery == 1 {
STAGE_IRQ1
} else {
STAGE_IRQ2
};
if STAGE
.compare_exchange(stage, next_stage, Ordering::Release, Ordering::Acquire)
.is_err()
{
ctx.spsr_el1 |= SPSR_IRQ_MASK;
publish_secondary_error(ERR_STAGE, stage, STAGE.load(Ordering::Relaxed));
} else {
notify_peer();
}
true
}snippet sha256: 77cbb2c4f6d4…file sha256: 4decf8a3b6c7…
02 · Kapı kimlik kaydı
Operations sıra, kimlik ve başlık bağı
tam Operations kaydıL29506–L29594
website/src/lib/operations.ts::rpi5-g8g-counter-contract-corrected
{
id: "rpi5-g8g-counter-contract-corrected",
date: "2026-08-21",
sequence: 83,
status: "fixed",
title: "G8g counter sözleşmesi fiziksel CNTVCT nedenselliğiyle düzeltildi",
summary:
"Sıra 84 dormant runtime ön incelemesi, Sıra 81 sentetik CPU0 next-CVAL sözleşmesinin gerçek timer indüksiyonu ve G8b fiziksel geçmişiyle üretilemeyeceğini fail-closed yakaladı. Eski START+one-period/540540000 bağı reddedildi; checked start+(ticks+1)×period, nested G8b causal bounds, BOOT8F UART sonrasındaki CPU0 capture, strict CPU1_START>capture ve ikinci IRQ sonrasındaki third-deadline kontrolü tek zincirde bağlandı. Canonical G8g fixture artık CPU0 START/LAST/NEXT=0/594540000/595080000, CAPTURE=603000000, CPU1 START=603000100 ve third-check delta=100 taşır. G8f 9/9 + G8g source 7/7 + G8g UART 11/11 = 27/27, full simulation 206/206, workspace check ve canonical CLI PASS; capture equality mutasyonu exit 1 verdi. Bu bir contract/parser düzeltmesidir: workspace'teki dormant runtime taslağı kabul edilmedi ve production'a bağlı değildir; image, microSD, UART ve fiziksel BOOT8G hâlâ STOP'tur.",
evidence: [
"Değişmeyen fiziksel prerequisite Sıra 80 BOOT8F raw'ıdır: 17.363 B / e70e1a9a2cf35f9079ee1b1a73d992106bf5ee9a19f1bbf2628582e836ea5068, direct validator PASS ve SCOPE=QUIESCENT_ATOMIC_HANDOFF_ONLY.",
"Reddedilen eski bağıntı CPU0_START=540000000, CPU0_PERIOD=540000, CPU0_NEXT_CVAL=540540000 ve CPU0_TICKS=1101 idi; 1101 işlenmiş tick ile yalnız ilk deadline'ı next-CVAL saydığı için fiziksel olarak imkânsızdır.",
"Corrected allocation-free helper'lar checked `last=start+ticks×period` ve `next=start+(ticks+1)×period` uygular; zero-period ile checked-add/multiply overflow açık hata olur.",
"Nested G8b bağı exact period equality, `last_processed(cpu0_start, period, g8b.start_ticks) <= g8b.timer_start_count` ve `g8b.timer_fired_count <= CPU0_CAPTURE_COUNT` nedenselliğini zorunlu kılar.",
"Canonical CPU0 START/LAST/NEXT=0/594540000/595080000; BOOT8F final UART çıkışından sonraki CPU0_CAPTURE_COUNT=603000000 ve CPU1_START=603000100 strict büyüklük sırasındadır.",
"CPU1 deadline zinciri FIRST=603540100, IRQ1 FIRED/NEXT=603540200/604080100, IRQ2 FIRED/NEXT=604080220/604620100 ve THIRD_CHECK_COUNT=604620200'dir; third_check_delta=100 < period=540000.",
"İki IRQ, timer off+masked final state ve third-deadline kontrolü herhangi bir G8g UART satırından önce tamamlanmalıdır; G8G0 ile BOOT8G arasındaki `[SEC` CPU0 marker'ı fail-closed reddedilir.",
"Final contract exact 4.896 B / ae128a6daeac810e291195c17f12ae05ae474ac46e91399c7628c1b92d3c53da; strict parser 35.712 B / 86989a92613fd4d20aea8300fb5e80de66df2e1fe2b1dc88f88952b37877a3e9.",
"UART adversarial test exact 24.246 B / 2c00c3dc2c652f8334c6f60a6abc65ff544304daa181d72fc5a251e33210f9c6; canonical suffix exact 4 satır, 1.734 B / 9996bfc9e620e50be5ac288b103a488a60a1c2df940f2b80c0cdb69f2813ab7d.",
"CLI validator exact 1.365 B / 543c3fdc8380dbe5873fe30d0126c7c1884ca3a4ba3f4282f18036fbb572f7dc; canonical çıktı `third_check_delta=100` ile exit 0 verdi.",
"`make verify-rpi5-g8g-contract`: G8f UART 9/9 + G8g source 7/7 + G8g UART 11/11 = 27/27 PASS ve example check PASS.",
"Tam simulation matrisi 206/206, `cargo check --workspace`, `cargo fmt --all -- --check` ve `git diff --check` PASS verdi; mevcut kernel warning'leri hata değildir.",
"Capture-equality adversarialı CPU1_START=CPU0_CAPTURE_COUNT ile exit 1 verdi ve strict chronology hatasını yayımladı; old one-period, coordinated START=540m, overflow, split-frequency, early/late-third-check ve SEC mutasyonları da reddedildi.",
"Production reachability taraması main, G8f ve exception dispatcher'da G8g wiring olmadığını doğruladı; unaccepted runtime draft'ı rustc production modülü veya physical behavior değildir.",
"Sıra 83 correction proof exact 8.379 B / 86a78d15856f0fa7387b214c8ea52dbbd525da4b2674b449f622befa10604727; corrected staged proof 7.446 B / 60e2f9cbc8d99c8c7e971c975255370425b13188d3f2793ab69b0e63aab96d29.",
"Corrected timer-storage proof exact 6.709 B / b633b904c1f9a441b791303543bf201d8e33f053b05f3706a0b47cb73bb6e7d8; Sıra 84–93 planlı roadmap exact 21.744 B / 959a5a7f74b7f6c0059733399b3a872bde9f0a2c6476e9c5d40a0bb30917bb9d.",
],
terminalSessionsNote:
"Oturumlar corrected host contract/parser ve production-unreachable sınırını gösterir. Sentetik PASS, dormant runtime kabulü, yeni image veya fiziksel BOOT8G değildir.",
terminalSessions: [
{
id: "g8g-counter-causality-correction",
title: "CPU0 next-CVAL, G8b causal geçmiş ve common-CNTVCT capture",
commandLines: [
"audit timer induction and nested G8b chronology",
"replace impossible START+one-period fixture with checked (ticks+1)*period",
"bind BOOT8F-UART→CPU0 capture→CPU1 start and third deadline",
],
outputLines: [
"old CPU0 540000000/540540000 at ticks1101=REJECTED",
"CPU0 last/next/capture=594540000/595080000/603000000",
"CPU1 start=603000100 > capture · d3/third=604620100/604620200",
"cross-era G8b causal bounds=PASS · physical contract=GO",
],
exitCode: 0,
outputMode: "selected",
},
{
id: "g8g-corrected-validator-matrix",
title: "Corrected strict parser, adversarial matris ve canonical CLI",
commandLines: [
"make verify-rpi5-g8g-contract",
"cargo test -p aselsan_microkernel_simulation",
"cargo run --quiet -p aselsan_microkernel_simulation --example verify_rpi5_g8g_log -- <canonical-chain>",
],
outputLines: [
"G8f UART 9/9 + G8g source 7/7 + G8g UART 11/11=27/27 PASS",
"simulation full matrix=206/206 PASS",
"canonical CLI exit=0 · third_check_delta=100",
"CPU1_START=capture mutation exit=1 · fail-closed chronology error",
],
exitCode: 0,
outputMode: "complete",
},
{
id: "g8g-runtime-remains-unaccepted",
title: "Production reachability ve kaydırılmış kapı sınırı",
commandLines: [
"scan main, G8f and exception dispatcher for G8g production references",
"audit dormant draft against no-UART-between-IRQs and third-deadline requirements",
],
outputLines: [
"production_g8g_wiring=ABSENT",
"dormant draft=UNACCEPTED/UNLINKED",
"next authorized gate=Sequence 84 dormant runtime source TDD",
"layout/image/SD/UART/physical BOOT8G=STOP",
],
exitCode: 0,
outputMode: "selected",
},
],
limitations: [
"Bu kayıt corrected contract/parser/fixture host kanıtıdır; dormant G8g runtime, machine-code/layout veya fiziksel BOOT8G PASS değildir.",
"Workspace'teki `kernel/src/rpi5_g8g.rs` taslağı unaccepted ve unlinked'dir; main, G8f ve exception dispatcher G8g production referansı taşımaz.",
"Parser canonical fixture'ı sentetiktir. Capture'ın gerçek BOOT8F UART dönüşünden sonra, release'den önce alınması ve bütün G8g UART'ın IRQ1/IRQ2/third-check sonrasına bırakılması Sıra 84 source/runtime kapısında zorlanacaktır.",
"Yeni kernel image/package üretilmedi; microSD, UART, Debug Probe ve Pi güç durumuna dokunulmadı. Son fiziksel PASS Sıra 80 BOOT8F'tir.",
"Generic SMP, CPU1 preemption, runqueue, migration, TLBI, CPU2/CPU3, soak ve hotplug 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: 06bcebd173f2…file sha256: 9726dbf00f84…
Kayıtlı yürütme/kanıt komutu
audit timer induction and nested G8b chronologyRegistry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06