K1/MEM2: S133 EL0 return-witness bounded stability

//! S271 bounded synchronization policy for the S133 EL0 return witness and
//! its post-exit cancellation-absence audit.
//!
//! The OOM completion owner and the newly woken caller may have equal
//! effective vruntime. The owner therefore cannot assume that the caller has
//! already crossed the ordinary EL0 `SYS_WRITE` boundary or left the
//! scheduler's retired-task slot. This allocation-free step policy permits
//! bounded cooperative handoff until both conditions hold while keeping
//! exhaustion explicit and fail-closed.

pub const S271_EL0_IPC_RETURN_WAIT_YIELD_BUDGET: usize = 128;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum S271El0IpcReturnWaitDecision {
    Observed { completed_yields: usize },
    Yield { completed_yields: usize },
    Exhausted { completed_yields: usize },
}

pub const fn decide_s271_el0_ipc_return_wait(
    observed: bool,
    completed_yields: usize,
) -> S271El0IpcReturnWaitDecision {
    if observed {
        return S271El0IpcReturnWaitDecision::Observed { completed_yields };
    }
    if completed_yields >= S271_EL0_IPC_RETURN_WAIT_YIELD_BUDGET {
        return S271El0IpcReturnWaitDecision::Exhausted { completed_yields };
    }
    S271El0IpcReturnWaitDecision::Yield {
        completed_yields: completed_yields + 1,
    }
}

#[test]
fn s271_policy_advances_one_bounded_yield_at_a_time() {
    for completed_yields in 0..S271_EL0_IPC_RETURN_WAIT_YIELD_BUDGET {
        assert_eq!(
            decide_s271_el0_ipc_return_wait(false, completed_yields),
            S271El0IpcReturnWaitDecision::Yield {
                completed_yields: completed_yields + 1
            }
        );
    }
}

  {
    id: "k1-mem2-s271-bounded-s133-el0-return-witness-stability-partial",
    date: "2026-08-26",
    sequence: 271,
    status: "fixed",
    umbrella_status: "partial",
    title: "K1/MEM2: S133 EL0 return-witness bounded stability",
    summary:
      "S271, S270 sonrasında gözlenen aralıklı S133 completion-owner/scheduler tie-order yarışını exact EL0 SYS_WRITE cancellation-return witness'ını gevşetmeden kapattı. Production policy exact task-id ve exact user-copy marker'ı arar; marker hazırsa sıfır yield, gecikirse adım başına tek cooperative yield ve en fazla 128 yield uygular, sınırda eksik tanık fail-closed panic olur. Kernel marker taklit edemez, bekleme sınırsız değildir. S270 reader guard kusuru değildir; S270'nin ilk QEMU repeat-stability iddiası geri çekilmiş, S238–S270 doğru dependency toplamı 34 grup / 447/447 olarak düzeltilmiştir. Dar runtime kabulü PASS, K1/K2/MEM0–MEM2 umbrella PARTIAL kalır.",
    evidence: [
      "S271 policy/source-lock odak kapısı iki byte-equal koşuda 10/10 PASS verdi: 125 B / SHA-256 7742173cc9d98f4cbe90debabdf83ee6b5d3e9e965e25428a46d090582275222. Immediate observation, 0→128 tek-adım ilerleme, exact-boundary observation ve exhaustion fail-closed yolları ayrı doğrulandı.",
      "Kanonik RED kanıtı korunur: 32081 B raw / SHA-256 f55f9677381ff9f7e7ffe12ac1fdbcb7f1303584824bcbea6fda695b52520acb; frozen assertion, S133 completion owner'ı exact EL0 SYS_WRITE witness'ından önce seçildiğinde panic veriyordu. S271 bunu S270 guard hatası olarak sınıflandırmaz.",
      "Production policy allocation-free'dir: exact expected task ve exact user-copy marker zorunludur; marker mevcutsa yield=0, gecikmeli path'te her adım bir yield, bütçe 128, exact budget boundary kabul ve bütçe sonrası marker yoksa FAIL_CLOSED_PANIC. Kernel-forged marker ve unbounded wait yoktur.",
      "S270 source-lock iki byte-equal koşuda 12/12 PASS olarak korunur. S270 taslağındaki 34 grup / 452/452 aritmetik kaydı kanonik değildir; S238–S270 doğru alt toplamı 34 grup / 447/447'dir ve ilk QEMU pair-stability claim'i S271 ile geri çekilmiştir.",
      "S238–S271 dependency matrisi iki byte-equal koşuda 35 grup / 457/457 PASS verdi: ham özet 3324 B / SHA-256 c4460c93d03760201859ca3f6f4f1b986747435869f8004bec95ad0782571890; süre-normalize 3394 B / SHA-256 64352eb20f3435757cdb6a15894000b00f326354af2f17fe43d39681f10a421f.",
      "Erken scheduler-race stress'i aynı final QEMU ELF'iyle 12 bağımsız 3 saniyelik koşuda 12/12 PASS verdi: toplam raw 2949618 B, S271 marker=12, kernel panics=0; 12 raw hash manifesti 2160 B / SHA-256 352aac96c8dd33cdf53333ea411f89f8d339b26875341a90a3d45e79ff436f42.",
      "İki bağımsız tam 32 saniyelik qemu-smoke koşusu PASS verdi: raw 1797771 B / SHA-256 69f10b20ce93d5cfd0b2316fa182d43b49b9ded509b2eb4569eec93d02498411 ve 2062575 B / SHA-256 157d23bccff1ea6611842b528e0fadcba82a918f113c63cf9bd93f778b9ff932. Wrapper 1551 B / SHA-256 527ef12c2bc56140e14e13be445f78c8e38872febc9849afcfacd499238ff966 byte-equal kaldı; observed YIELDS=0/128.",
      "QEMU acceptance zinciri korundu: W^X 31/31, S130–S154, S154 32 round / 1024 retired / SLA PASS, RuntimePmm 6144→6144, active allocations 0→0, EL0 return x4096, IPC 20/20, SEC5 ve kernel faults=0.",
      "board-qemu, board-rpi5 ve board-rpi5,smp AArch64 check'leri ikişer byte-equal PASS verdi; warning header envanteri 291 / 711 / 711'dir, zero-warning iddiası yoktur. Combined board profile negative check fail-closed exit 101 / 16 compiler error / 17 error header / 18556 B ile korunur.",
      "Manifest-aware workspace audit'i iki koşuda 233 grup / 2217 PASS / 0 fail / 7 tarihsel filtre verdi. Filtresiz workspace exit 101 ile frozen S96 exceptions.S identity mismatch'te durur; expectation gevşetilmedi. S271 physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S271=NO.",
      "Canlı marker: S271_BOUNDED_S133_EL0_RETURN_WITNESS_STABILITY_EXACT_TASK_AND_USER_COPY_MARKER_YIELDS_0_TO_128_FAIL_CLOSED_NO_KERNEL_FORGED_MARKER_QEMU_EARLY_RACE_12_OF_12_FULL_2_OF_2_PANICS_0_S238_S271_35_GROUPS_457_OF_457_S270_CORRECTED_SUBSET_34_GROUPS_447_OF_447_WORKSPACE_2217_PASS_7_HISTORICAL_G8H_ASSERTIONS_RED_PHYSICAL_DEVICE_OPERATIONS_0_RUNBOOK_EXECUTED_IN_S271=NO_VERIFIED.",
    ],
    commands: [
      "cargo test --quiet -p aselsan_microkernel_simulation --test runtime_oom_el0_ipc_return_witness_stability -- --test-threads=1",
      "make verify-qemu",
    ],
    terminalSessions: [
      {
        id: "k1-mem2-s271-bounded-s133-el0-return-witness-stability",
        title: "K1/MEM2 S271 bounded S133 EL0 return-witness stability",
        commandLines: [
          "cargo test --quiet -p aselsan_microkernel_simulation --test runtime_oom_el0_ipc_return_witness_stability -- --test-threads=1",
          "make verify-qemu",
        ],
        outputLines: [
          "test result: ok; S271 focused 1 group / 10 passed; 0 failed",
          "policy: exact task + exact user-copy marker · immediate YIELDS=0 · delayed one yield/step · budget=128 · exhaustion=FAIL_CLOSED_PANIC",
          "QEMU early-race stress: 12/12 PASS · S271 markers=12 · kernel panics=0",
          "QEMU full regression: 2/2 PASS · YIELDS=0/128 · W^X 31/31 · S154 retired 1024 · IPC 20/20 · SEC5 · faults=0",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S271 yalnız S133 acceptance fixture'ının scheduler tie-order yarışını bounded ve fail-closed biçimde stabilize eder; production IPC cancellation sonucu, exact EL0 witness veya fiziksel kabul gevşetilmez.",
    limitations: [
      "S238–S270 correct dependency subset is 34 groups / 447/447; the earlier S270 452 arithmetic claim and initial QEMU pair-stability claim are historical corrections, not acceptance evidence.",
      "S270 scheduler read coverage 42/111 ve 69 unrouted olarak kalır; writer paths, production exclusive wrapper, provider authority ve whole-scheduler exclusion açıktır.",
      "Tam workspace GREEN değildir: frozen S96 exceptions.S identity mismatch korunur ve expectation gevşetilmemiştir.",
      "Physical RPi, CPU2/CPU3, hotplug, long soak ve Generic SMP açık kalır; S271 physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S271=NO.",
    ],
  },