Database

Database

Linear (QTT) + refinement bindings for sqlite3 — a state-safe database API. Raw sqlite3 is error-prone in two ways this library closes: 1. **Transaction discipline (linearity).** A transaction must be committed XOR rolled back — exactly once — and the connection closed exactly once. Forget the commit and your writes silently vanish; touch the connection after close and you get ``ProgrammingError: Cannot operate on a closed database``. These are linear-resource rules, so ``Conn`` and ``Txn`` are multiplicity-1 handles: the type checker forces a complete, well-ordered lifecycle and rejects a forgotten commit (``LinearUnusedError``) or a use-after-commit / double-close (``LinearUsedTooManyTimesError``). 2. **State (typestate).** The *kind* of handle encodes the connection state. You cannot ``execute`` on a plain ``Conn`` (you must ``begin`` a ``Txn`` first), nor ``close`` a ``Txn`` (you must ``commit``/``rollback`` back to a ``Conn``). Illegal orderings simply do not type-check. Plus ordinary refinements: non-empty paths and SQL, non-negative row counts. The lifecycle threads a linear handle exactly like libraries/Socket.ae: let 1 c0 := connect "app.db" in let 1 t0 := begin c0 in let 1 t1 := execute "INSERT INTO log VALUES ('x')" t0 in let 1 c1 := commit t1 in # MUST commit or rollback — exactly once close c1 # MUST close — and t0/t1 are now unusable

Imports

open Array;

Types

Conn

(type) linear

linear type Conn

Txn

(type) linear

linear type Txn

Rows

(type)

type Rows

Functions

sqlite3

def sqlite3 : Unit

read_all

Runs a SELECT against `path` and returns every row. Both arguments must be non-empty.

def read_all (path : String | path ≠ "") (sql : String | sql ≠ "") : {r : Rows | row_count r ≥ 0}

num_rows

Number of rows returned. Pinned to the `row_count` measure; non-negative.

def num_rows (r : Rows) : {n : Int | n = row_count r && n ≥ 0}

is_empty

True exactly when the result set is empty. Tied to `row_count`.

def is_empty (r : Rows) : {b : Bool | b = row_count r = 0}

connect

Opens a connection to `path`. `isolation_level=None` puts sqlite3 in autocommit mode so the explicit BEGIN / COMMIT / ROLLBACK below are honored exactly as written. Each call yields a fresh connection.

def connect (path : String | path ≠ "") : Conn

begin

Begins a transaction, advancing the connection from `Conn` to `Txn`.

def begin (1 c : Conn) : Txn

execute

Executes one statement inside the transaction and threads the `Txn` onward. `sql` must be non-empty.

def execute (sql : String | sql ≠ "") (1 t : Txn) : Txn

commit

Commits the transaction and returns the connection (now outside any txn) so it can be reused or closed. Consumes the `Txn`.

def commit (1 t : Txn) : Conn

rollback

Rolls the transaction back, discarding its writes, and returns the connection. Consumes the `Txn`.

def rollback (1 t : Txn) : Conn

close

Closes the connection. Consumes the `Conn`, so it cannot be used afterward.

def close (1 c : Conn) : Unit

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