Typed stream channels and P3 async extensions for Kiln integration

[avrabe]

Context

WASM P3 async primitives (stream, future, task management) map directly to Gale's verified RTOS modules. RFC #46 (Kiln architecture) specifies that Gale backs these primitives on embedded targets. This issue tracks the extensions needed to make Gale P3-ready.

Current State

Gale's 39 verified modules already cover the fundamentals:

• ring_buf (RB01-RB08) → backing for stream<T>
• event (EV01-EV08) → backing for future<T>
• poll (PL01-PL08) → backing for task.wait/task.poll
• sem (P01-P10) → backing for task.backpressure
• sched (SC01-SC16) + thread (TH01-TH06) → backing for task management
• timer (TM01-TM08) + timeout (TO01-TO08) → backing for cancellation

Extensions Needed

1. Typed Ring Buffer (extend ring_buf)

P3 stream<T> carries typed elements, not raw bytes. Extend ring_buf with type-aware element boundaries:

pub struct TypedRingBuf<const ELEM_SIZE: usize, const CAPACITY: usize> {
    inner: RingBuf<{ ELEM_SIZE * CAPACITY }>,
}

impl<const E: usize, const C: usize> TypedRingBuf<E, C> {
    pub fn write_element(&mut self, data: &[u8; E]) -> Result<(), Full>;
    pub fn read_element(&mut self, buf: &mut [u8; E]) -> Result<(), Empty>;
    pub fn elements_available(&self) -> usize;
    pub fn space_available(&self) -> usize;
}

Verification: Extend RB01-RB08 to cover:

• RB09: Element boundary alignment (no partial element reads)
• RB10: Typed capacity invariant (available + space = CAPACITY in element count)
• RB11: Zero-copy element reference (borrow without copy for same-memory components)

2. Backpressure Gate (extend sem + event)

P3 task.backpressure(enabled: bool) needs a verified gating primitive:

pub struct BackpressureGate {
    sem: Semaphore,       // flow control (P01-P10 verified)
    enabled: AtomicBool,  // fast-path bypass
}

impl BackpressureGate {
    pub fn enable(&self);   // stop host from calling component
    pub fn disable(&self);  // resume host calls
    pub fn is_enabled(&self) -> bool;
    pub fn wait_until_ready(&self, timeout: Timeout) -> Result<(), TimedOut>;
}

Verification: BP01-BP04 properties:

• BP01: enable() prevents new host invocations
• BP02: disable() allows pending invocations to proceed
• BP03: wait_until_ready blocks iff enabled
• BP04: no message loss during backpressure transitions

3. Waitable Event Aggregator (extend poll)

P3 task.wait returns typed events. Extend poll with event type tagging:

#[repr(u32)]
pub enum WaitableEventType {
    None = 0,
    Subtask = 1,
    StreamRead = 2,
    StreamWrite = 3,
    FutureRead = 4,
    FutureWrite = 5,
    Cancelled = 6,
}

pub struct WaitableEvent {
    pub event_type: WaitableEventType,
    pub join_id: u32,
}

Verification: Extend PL01-PL08:

• PL09: Event type is always valid (no undefined event codes)
• PL10: Join ID corresponds to a registered waitable
• PL11: Cancelled events are delivered exactly once

4. MPU-Protected Shared Regions for Zero-Copy Streams

P3 spec plans zero-copy stream optimization. On ARM targets with MPU:

pub struct SharedStreamRegion {
    mem_domain: MemDomain,  // MD01-MD06 verified
    ring_buf: TypedRingBuf<ELEM_SIZE, CAPACITY>,
}

Two components can share a ring buffer in an MPU-protected memory region:

• Writer has write access to write pointer + data region
• Reader has read access to read pointer + data region
• Neither can access the other's stack or heap
• Hardware-enforced isolation with zero-copy data transfer

Verification: Extend MD01-MD06 with stream-specific properties.

5. Callback Dispatch Table

P3 callback lifting mode: host calls component's callback on events. Gale needs:

pub struct CallbackTable<const MAX_CALLBACKS: usize> {
    entries: [(WaitableEventType, FnPtr); MAX_CALLBACKS],
    count: usize,
}

Registered at component init, dispatched by the Gale scheduler when events fire.

Verification Strategy

All extensions follow Gale's triple-track:

1. Verus: SMT verification of new properties
2. Rocq: Extend abstract invariant proofs for typed channels
3. Kani: Bounded model checking harnesses for new APIs
4. Functional tests: cargo test + Zephyr QEMU + Renode

Connects to

• Kiln P3 runtime (kiln#230) — Gale provides no_std backend for P3 intrinsics
• Meld P3 lowering (meld#94) — Meld generates code that calls these primitives
• cFS Software Bus (kiln#226) — cFS messages flow through these streams

Priority

High — Gale is the formally verified foundation for P3 async on embedded targets.

[avrabe]

Recommendation: Move to Kiln

After investigation, the typed stream/backpressure/waitable primitives are WASM Component Model concepts that belong in kiln-builtins, not the RTOS kernel.

Gale's role is replacing existing Zephyr C code with verified Rust — every module maps 1:1 to a Zephyr kernel source. A "typed channel" has no Zephyr counterpart and would be inventing new RTOS abstractions for a single consumer.

Created pulseengine/kiln#233 to track the Kiln-side implementation, which composes Gale's already-verified primitives (ring_buf, msgq, event, poll, sem) at the runtime level.

Gale's contribution to P3 is keeping the verified foundation solid — the building blocks Kiln needs are already here and ASIL-D verified.

This issue can be closed — the work is tracked in kiln#233.