Reader

Linear (QTT) byte reader — open → read* → close, inspired by LiquidJava's ``InputStreamReader`` refinements. Unlike ``Path.read`` (one-shot whole-file), this API exposes a streaming handle. ``reader_open`` tracks whether the stream is still live; ``read`` returns a code in ``[-1, 255]`` (``-1`` = EOF) and threads the open reader; ``close`` consumes it. let 1 r0 := open_reader path in let step := read r0 in let code := read_code step in let 1 r1 := read_reader step in close r1;
Table of Contents

Types

Reader

(type) linear
linear type Reader

ReaderStep

(type)
Unrestricted token after ``read``: byte/EOF code plus the live reader.
type ReaderStep

Functions

open_reader

Open ``path`` for binary reading. Path must be non-empty.
def open_reader (path : String | path ≠ "") : {r : Reader | reader_open r = True}

read

Read one byte from an open reader. Returns ``-1`` at EOF, else ``0..255``. Consumes the reader and recovers it via ``read_reader``.
def read (1 r : Reader | reader_open r = True) : {s : ReaderStep | step_code s ≥ 0 - 1 && step_code s ≤ 255}

read_code

def read_code (s : ReaderStep) : {n : Int | n = step_code s && (n ≥ 0 - 1 && n ≤ 255)}

read_reader

def read_reader (s : ReaderStep) : {r : Reader | reader_open r = True}

close

Close an open reader. Consumes the handle.
def close (1 r : Reader | reader_open r = True) : Unit

Uninterpreted

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

reader_open

uninterpreted
def reader_open : (r : Reader) → Bool

step_code

uninterpreted
def step_code : (s : ReaderStep) → Int