The store layer

A Geas contract can be backed by a database. The contract declares the table shape it needs as a schema, binds a live database through a dsn vow, and its pledges read and write rows through the store standard library. The database sits behind the contract, not in front of the host: a host signs, fulfills, and breaks a store backed contract with the same calls it always used, and the storage never shows through the ABI.

This page uses skeleton/ledger.geas from the repository as its running example.

Declaring the shape

A store backed contract declares its table beside its vows:

import std.store

LedgerError is either NoSuchAccount or StoreFailed or Insufficient

contract Ledger {
    vow dsn: String = "file:ledger.db"

    schema Accounts {
        id: Int
        balance: Float
        owner: String
    }
}

The dsn vow names the data source, a file path or URI for SQLite. It is a vow like any other: immutable from the sign, overridable at the sign, so a host points the ledger at a temp database with a sign time override and nothing more. A contract with a schema but no dsn vow fails to sign.

A schema names a table and its columns, each column a scalar type: Int, UInt, Float, Bool, Byte, Char, or String. A composite column is a type error; a contract that wants structure composes it in the pledge from several columns or several schemas. The first column of a schema is its primary key. A schema also stands up a record, so a row a pledge reads is an ordinary record whose fields are the columns in declaration order.

Reconciled at sign

The schema is vow shaped: immutable, locked at sign, and load bearing at sign. When the contract signs, the runtime reconciles every declared schema with the live database on the bound dsn. An absent table is created to match the schema exactly, so a fresh database is a working one with no setup step. A present table is validated column for column, name and type, and a table whose shape disagrees fails the sign. The schema joins the contract’s shape hash, so a changed column fails a stale host’s sign the way a changed pledge does.

Reading and writing rows

A pledge body reads and writes through Store, naming a schema in its own contract. The surface is small and every operation returns a Result:

operation	shape
Store.find(S, key)	one row by primary key, Result<Option<Row>, StoreError>
Store.query(S, predicate)	every matching row, Result<List<Row>, StoreError>
Store.insert(S, row)	add one row
Store.update(S, key, row)	replace a row’s columns by key
Store.delete(S, key)	remove a row by key
Store.count(S, predicate)	how many rows match, counted by the store
Store.sum(S, column, predicate)	the column totaled by the store, zero over no rows
Store.min(S, column, predicate)	the smallest matching value, None over no rows
Store.max(S, column, predicate)	the largest matching value, None over no rows
Store.avg(S, column, predicate)	the mean of a numeric column as Float, None over no rows

The ledger’s balance pledge reads one row, and a hit and a miss are both Ok answers:

pledge balance(id: Int) -> Result<Float, LedgerError> {
    return match Store.find(Accounts, id) {
        Ok(Some(row)) -> Ok(row.balance)
        Ok(None) -> Err(NoSuchAccount)
        _ -> Err(StoreFailed)
    }
}

Writing is the same shape. open inserts the schema’s record as a row:

pledge open(id: Int, owner: String, amount: Float) -> Result<Bool, LedgerError> {
    let row = Accounts { id: id, balance: amount, owner: owner }
    return match Store.insert(Accounts, row) {
        Ok(_) -> Ok(true)
        _ -> Err(StoreFailed)
    }
}

Every value bound into an operation crosses as a parameter, positionally bound in the prepared statement, never concatenated into text, so a string column holding '; drop table is a string and nothing else.

Predicates

Store.query, Store.count, and the aggregates all read one predicate grammar: comparisons with ==, !=, <, <=, >, and >=, joined with && and ||, with && binding tighter as everywhere in the language. The left side of every comparison is a bare column name resolved against the schema at compile time, never a value; the right side is an ordinary expression checked against that column’s declared type.

pledge owned_above(owner: String, min: Float) -> Result<Float, LedgerError> {
    return match Store.query(Accounts, owner == owner && balance >= min) {
        Ok(rows) -> {
            let mut sum = 0.0
            for row in rows {
                sum = sum + row.balance
            }
            Ok(sum)
        }
        _ -> Err(StoreFailed)
    }
}

The owner on the left of == is the column and the owner on the right is the parameter: the left of a comparison is always a column and never a value, so sharing the name is unambiguous.

A leading ! negates any subtree, and the compiler eliminates it before the store is ever asked: ! flips a comparison at the leaf and distributes over && and || by De Morgan’s law, so !(balance <= lo || balance >= hi) runs as balance > lo && balance < hi and the store never learns a ! was written.

pledge others(who: String) -> Result<Int, LedgerError> {
    return match Store.count(Accounts, !(owner == who)) {
        Ok(n) -> Ok(n)
        _ -> Err(StoreFailed)
    }
}

Ordering and limits

A trailing asc(column) or desc(column) orders the matching rows by one column, and a limit(n) after the order bounds the answer to at most n rows. A limit without an order is refused at compile time, because the rows a bound cuts are defined only once an order says which come first. The count is an ordinary Int expression, a literal or a runtime value alike:

pledge top_owners(min: Float, k: Int) -> Result<String, LedgerError> {
    return match Store.query(Accounts, balance >= min, desc(balance), limit(k)) {
        Ok(rows) -> {
            let mut s = ""
            for row in rows {
                s = s + row.owner
            }
            Ok(s)
        }
        _ -> Err(StoreFailed)
    }
}

Aggregates

Store.count, Store.sum, Store.min, Store.max, and Store.avg answer without materializing rows into the process: the store computes behind the boundary and hands back only the number. A sum over no rows is the zero of the column’s own type, because an empty ledger owes nothing. The extremes and the mean have no zero to stand on, so min, max, and avg answer an Option, None over the empty set:

pledge midpoint(lo: Float) -> Result<Option<Float>, LedgerError> {
    return match Store.avg(Accounts, balance, balance >= lo) {
        Ok(o) -> Ok(o)
        _ -> Err(StoreFailed)
    }
}

Transactional subcontracts

A group of writes that must all land or all vanish is a transactional subcontract, the unit the language already had for all or nothing. The ledger’s transfer is two writes in one episode:

subcontract Transfer transactional {
    pledge debit(id: Int, amount: Float) -> Result<Unit, LedgerError> {
        return match Store.find(Accounts, id) {
            Ok(Some(row)) -> {
                if row.balance < amount {
                    return Err(Insufficient)
                }
                match Store.update(Accounts, id, Accounts { id: id, balance: row.balance - amount, owner: row.owner }) {
                    Ok(u) -> Ok(u)
                    _ -> Err(StoreFailed)
                }
            }
            Ok(None) -> Err(NoSuchAccount)
            _ -> Err(StoreFailed)
        }
    }

    pledge credit(id: Int, amount: Float) -> Result<Unit, LedgerError> {
        return match Store.find(Accounts, id) {
            Ok(Some(row)) -> match Store.update(Accounts, id, Accounts { id: id, balance: row.balance + amount, owner: row.owner }) {
                Ok(u) -> Ok(u)
                _ -> Err(StoreFailed)
            }
            Ok(None) -> Err(NoSuchAccount)
            _ -> Err(StoreFailed)
        }
    }
}

The transaction opens on the first fulfillment of a pledge in the subcontract and every write inside it is buffered. It commits the moment the subcontract completes, its last pledge latching Ok, and it rolls back the instant any pledge in it returns Err or the contract breaks first. A debit past the balance is Err(Insufficient) and a credit against a missing account is Err(NoSuchAccount), each the ledger’s own business rolling the whole episode back so neither write survives.

Because a transaction is one episode and not a latch, a pledge in a transactional subcontract is fulfilled at most once; a second call after commit or rollback is a state error. Loose pledges outside any transactional subcontract run in autocommit, each store operation its own implicit transaction.

Two kinds of failure

A contract’s own rules, an overdraft, an unknown id, stay values in the contract’s own error type, the way Errors as values describes. A backend failure the runtime cannot complete, a lost connection, a full disk, a refused constraint, is a store status delivered through the wait the host already reads. The status is for the store failing the runtime, not for the contract failing its business.

Invisible across the ABI

The reference backend is SQLite, vendored as the amalgamation and compiled into libgeasrt, so the store needs no server and store tests are hermetic. The storage is invisible across the C ABI: discovery, signing with a dsn override, fulfillment through a future, and break are the same five moves a host makes against any contract, and a row read from a table behaves exactly like a value computed in memory. sign opens the connection and reconciles the schemas; break rolls back any open transaction, closes the connection, and reclaims the heap, in that order.

Postgres is planned behind the same store interface; a server backend adds a driver, not a language change. Migrations are not in v1: a schema reconciles by create or validate, and a divergent table fails the sign rather than pretending to migrate.

Where to go next

• Contracts and the lifecycle for the subcontract and policy machinery transactions build on.
• Errors as values for the split between contract errors and runtime statuses.
• Interop for driving the ledger from C and Python.
• Reference for the normative store rules.