Execute

Execute :: # (opaque)

Platform-independent execution. The caller owns the connection and gives one call exclusive access for its whole exchange. There are no implicit retries.

request! : Config, Request(value, decode_err), ByteIo(read_err, write_err) => Try(value, Error(read_err, write_err, decode_err))

Rejection leaves the stream untouched. Server/semantic errors follow a complete reply and leave framing aligned. They do not undo command effects.

batch! : Config, Batch(value, decode_err), ByteIo(read_err, write_err) => Try(value, [RequestRejected(ValidationError), ExchangeFailed(ExchangeError(read_err, write_err)), BatchDecodeFailure(decode_err), ReplyCountMismatch({ expected : U64, actual : U64 })])

no_reply! : Config, NoReply, { write_all! : List(U8) => Try({  }, write_err) } => Try({  }, [RequestRejected(ValidationError), WriteFailed(write_err)])

Write-only execution on explicitly suppressed replies. There is no reader capability and no reply-decoder error in this function's type.

disposition : Error(read_err, write_err, decode_err) -> Disposition

batch_disposition : [RequestRejected(ValidationError), ExchangeFailed(ExchangeError(read_err, write_err)), BatchDecodeFailure(decode_err), ReplyCountMismatch({ expected : U64, actual : U64 })] -> Disposition

Same rule for batch! outcomes: discard only on a transport failure. The complete wire batch is drained before any decoder runs, so decode and count failures leave framing aligned.

Read : [Data(List(U8)), End]

ByteIo : {
    read! : U64 => Try(Read, read_err),
    write_all! : List(U8) => Try({  }, write_err),
}

ValidationError : [
    CommandLimitExceeded({ actual : U64, limit : U64 }),
    RequestByteLimitExceeded({ limit : U64 }),
]

ExchangeError : [
    WriteFailed(write_err),
    ReadFailed(read_err),
    ConnectionClosed({ expected : U64, received : U64 }),
    ProtocolFailure({ completed : U64, error : DecodeError }),
    EmptyData,
    ReadLimitExceeded({ actual : U64, limit : U64 }),
    ResponseByteLimitExceeded({ limit : U64 }),
    UnexpectedData({ buffered : U64, expected : U64, received : U64 }),
]

Every failure here occurs after a write was attempted. Discard the stream; execution may already have occurred. Completed counts describe parsed wire replies, not proof that any remaining command was or was not executed.

Error : [
    RequestRejected(ValidationError),
    ExchangeFailed(ExchangeError(read_err, write_err)),
    ServerError(Bytes),
    ReplyDecodeFailure(decode_err),
]

Disposition : [Reuse, Discard]

Whether the connection is safe to reuse after a failure, or must be discarded. Only a transport failure (ExchangeFailed) corrupts framing; a validation rejection never wrote anything, and server/decoder errors follow a complete, framed reply. See the ExchangeError/Error invariants above. Pooling adapters map this onto their reuse/discard decision.