Module buffer 

Bounded buffers with backpressure.

Matches the Lean BoundedBuffer from lean/Runtime/Resources/BufferRA.lean. Ring buffer with configurable mode and backpressure policy.

Structs

BoundedBuffer

Bounded ring buffer for inter-role message passing.

BufferConfig

Configuration for a buffer.

SignedValue

Signed value payload used by authenticated transport layers.

Enums

BackpressurePolicy

Policy when a buffer is full.

BufferMode

Buffer delivery mode.

EnqueueResult

Result of attempting to enqueue a value.

SignedDequeueError

Signed dequeue failure.

SignedEnqueueResult

Result of signed enqueue attempts.

Functions

signed_dequeue_verified

Dequeue and verify one signed payload.

signed_enqueue

Enqueue one signed payload into per-edge signed buffers.

signed_enqueue_with_sequence

Enqueue one signed payload with explicit sequence number.

Type Aliases

SignedBuffer

Signed FIFO for a single edge.

SignedBuffers

Signed buffers indexed by sid-qualified edge.