Backpressure protocol for stream transformers: proven flow control

[avrabe]

Context

P3 has task.backpressure(enabled: bool) for flow control. When a component can't keep up with its input stream, it signals backpressure. On embedded (Gale), this maps to gale::sem (P01-P10 verified).

Problem

Without proven backpressure, a fast sensor producing stream can overwhelm a slow limit checker, causing either:

• Buffer overflow (if bounded) → lost data
• Unbounded growth (if Vec) → OOM

What to prove

1. Bounded buffer invariant

For each stream connection: buffer size ≤ MAX_BUFFER_SIZE (constant).
Prove: no execution path causes buffer to exceed MAX_BUFFER_SIZE.

2. No data loss under backpressure

When backpressure is asserted: producer blocks (doesn't drop data).
When backpressure is released: all buffered data is eventually consumed.

3. Liveness

Under fair scheduling: every reading eventually produces a result (no permanent stall).

Implementation

Gale-backed (embedded)

• stream → Gale ring_buf (RB01-RB08 verified, bounded capacity)
• Backpressure → Gale sem (P01-P10 verified, counting semaphore)
• When ring_buf full: writer blocks on semaphore (backpressure)
• When reader drains: semaphore signals (release backpressure)

Verus proof

Add to relay-lc:

ensures
    result.violation_count <= input_count, // output bounded by input
    // No internal buffering — evaluate() is synchronous per reading

The current engines are already safe: they process ONE reading at a time (no internal buffering). Backpressure is a HOST concern (Kiln/Gale), not an engine concern.

Connects to

• kiln#230: P3 async runtime (task.backpressure)
• gale#13: Typed stream extensions (ring_buf + sem)
• Spar AADL model (thread deadlines enforce processing rate)