ASELSANMicrokernel
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: 77cbb2c4f6d4file 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: 06bcebd173f2file sha256: 9726dbf00f84
Kayıtlı yürütme/kanıt komutu
audit timer induction and nested G8b chronology
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06