Writer

Linear byte writer — open → write* → close, counterpart to ``Reader``. Completes the streaming I/O story: ``Path.write`` is one-shot; this API exposes a live handle. ``writer_open`` tracks liveness; ``bytes_written`` is a ghost of cumulative payload length; ``close`` consumes the handle. let 1 w0 := open_writer path in let 1 w1 := write payload w0 in close w1;
Table of Contents

Types

Writer

(type) linear
linear type Writer

WriterPayload

(type)
Opaque host payload (``bytes`` at runtime).
type WriterPayload

Functions

payload_from_string

Build a payload from a non-empty string (UTF-8 bytes).
def payload_from_string (s : String | s ≠ "") : {p : WriterPayload | payload_len p > 0}

open_writer

Open ``path`` for binary writing (truncates). Path must be non-empty.
def open_writer (path : String | path ≠ "") : {w : Writer | writer_open w = True && bytes_written w = 0}

write

Append ``data`` to an open writer; increases ``bytes_written`` by ``payload_len``.
def write (data : WriterPayload) (1 w : Writer | writer_open w = True) : {out : Writer | writer_open out = True && bytes_written out = bytes_written w + payload_len data}

close

Close an open writer. Consumes the handle.
def close (1 w : Writer | writer_open w = True) : Unit

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

writer_open

uninterpreted
def writer_open : (w : Writer) → Bool

bytes_written

uninterpreted
def bytes_written : (w : Writer) → Int

payload_len

uninterpreted
def payload_len : (p : WriterPayload) → Int