examples/ledger/
Un registro contabile in SQLite, con i totali calcolati e verificati anche in Heroes.
- 1.011 righe
- 4 moduli
- usa C:
sqlite3.h
Il programma riusa un’istruzione preparata per inserire più righe in una transazione, un gruppo di operazioni salvate insieme. Usa anche una join per combinare dati di tabelle diverse. Gli importi sono numeri interi di centesimi. Il database e il codice Heroes calcolano i totali separatamente, poi il programma confronta i risultati.
Eseguilo
the book, as Heroes reads it
1 rent housing september -1200.00
2 salary income september 3100.00
3 food living market -42.50
4 food living bakery -7.80
5 books living two paperbacks -24.95
6 salary income a lesson 80.00
7 food living market -31.10
8 rent housing deposit back 600.00
9 books living a dictionary -55.00
10 food living market -29.40
balances, joined to each account's kind
account kind entries total
books living 2 -79.95
food living 4 -110.80
rent housing 2 -600.00
salary income 2 3180.00
sqlite and heroes, over the same rows
balances agree yes
total agrees yes
total 2389.25
rows agree yes
average agrees yes
average 238.92
living expenses, from the join
-190.75 agree yes
exit 0 · 29 righe
Il programma
# A ledger kept in SQLite, and every number checked twice.
#
# Corpus material (CLAUDE.md §9), M-corpus-depth's third family and the
# last of its nine programs. **What it is here for is a shape the corpus
# was measured not to have**: before it, the six directories that declared
# an `extern` group were 65 to 192 lines, every one a single module, and
# not one had a `variant`, a nested container, a generic or an
# `@`-parameter structure. FFI and "a real program" were disjoint sets.
# This one is four modules, binds eighteen SQLite functions, and puts the
# database behind a wall so the arithmetic can be tested without it.
#
# HOW IT IS CHECKED, and this is the whole method. There is no published
# answer for a book somebody invented, so the second opinion is built:
# **every total is computed twice, by two routes that share no line** —
# once by SQLite's own `sum(...) group by ...`, once by Heroes over the
# same rows — and the program prints `agree` only if they match cent for
# cent. Neither is the oracle. Two independent routes agreeing is a
# stronger claim than either alone, and it is the strongest one available
# when nobody else has published the answer.
#
# WHAT THE FIRST RUN FOUND, because a corpus program's first job is to
# report on the compiler. Two things, both in `db/sqlite.hero`'s own
# comments: an `extern` is not callable across a module boundary, so the
# module holding the header wraps every one of them; and a `ptr` may not be
# the element of a `T?`, so a handle is a one-field record — which then
# emitted C that clang warned about, filed and repaired as defect 009 the
# same hour.
use book/entry
use db/sqlite
use report/lines
function main()
opened = sqlite.opened()
if opened.is_err()
print("sqlite would not open a database: ", why_open(opened))
exit(1)
db: sqlite.Db @= opened.must()
built = build(db)
if built.is_err()
print("the ledger could not be built: ", err_text_of(built))
_ = sqlite.closed(@db)
exit(1)
shown = show(db)
if shown.is_err()
print("the ledger could not be read back: ", err_text_of(shown))
_ = sqlite.closed(@db)
exit(1)
_ = sqlite.closed(@db)
# The schema, the accounts and the entries — the entries through ONE
# prepared statement, bound and stepped and reset ten times, which is the
# shape `examples/sqlite/` does not have.
function build(db: sqlite.Db) -> ()?
sqlite.run(db, "create table account(name text primary key, kind text not null)")?
sqlite.run(db, "create table entry(id integer primary key, account text not null, memo text not null, cents integer not null)")?
# A transaction, so ten inserts are one unit — and so the program has a
# reason to name `begin` and `commit` rather than describing them.
sqlite.run(db, "begin")?
accounts: sqlite.Statement @= sqlite.prepared(db, "insert into account(name, kind) values (?, ?)")?
for a in entry.accounts()
sqlite.bind_text(statement: accounts, at: 1, text: a.name)?
sqlite.bind_text(statement: accounts, at: 2, text: a.kind)?
_ = sqlite.stepped(accounts)?
sqlite.reset(accounts)?
_ = sqlite.finalized(@accounts)
rows: sqlite.Statement @= sqlite.prepared(db, "insert into entry(id, account, memo, cents) values (?, ?, ?, ?)")?
for e in entry.book()
sqlite.bind_int(statement: rows, at: 1, value: e.id)?
sqlite.bind_text(statement: rows, at: 2, text: e.account)?
sqlite.bind_text(statement: rows, at: 3, text: e.memo)?
sqlite.bind_int(statement: rows, at: 4, value: e.amount.cents)?
_ = sqlite.stepped(rows)?
sqlite.reset(rows)?
_ = sqlite.finalized(@rows)
sqlite.run(db, "commit")?
return ok()
# The report, and the check. Four queries: the joined balances, the whole
# total, the busiest account, and the average — the last one the only float
# in the program.
function show(db: sqlite.Db) -> ()?
print("the book, as Heroes reads it")
for line in lines.book_lines(entry.book(), entry.accounts())
print(line)
print("")
print("balances, joined to each account's kind")
print(lines.BALANCE_HEADING)
from_db = queried_balances(db)?
mine = entry.balances(entry.book())
for b in from_db
kind = entry.kind_of(b.account, entry.accounts())?
print(lines.balance_line(b, kind))
print("")
# THE CHECK. SQLite grouped and summed the rows; Heroes grouped and
# summed the same rows without sharing a line with it. A difference
# here is a real disagreement about arithmetic, not a formatting
# accident, which is why it prints a verdict and not a number.
print("sqlite and heroes, over the same rows")
print(" balances agree ", verdict(same_balances(from_db: from_db, mine: mine)))
db_total = queried_int(db, "select sum(cents) from entry")?
print(" total agrees ", verdict(db_total == entry.total(entry.book()).cents))
print(" total ", entry.shown(entry.Amount(cents: db_total)))
db_rows = queried_int(db, "select count(*) from entry")?
print(" rows agree ", verdict(db_rows == entry.book().len()))
# The one place a float enters: SQLite's `avg` is a double. It is
# compared with a tolerance and the comparison says so, rather than
# asking two floating-point numbers to be equal.
average = queried_float(db, "select avg(cents) from entry")?
mine_average = to_f64(entry.total(entry.book()).cents) / to_f64(entry.book().len())
print(" average agrees ", verdict(near(a: average, b: mine_average)))
print(" average ", entry.shown(entry.Amount(cents: to_i64(average).must())))
# The join, asked of the database this time, so the two routes meet on
# the same question rather than on the same table.
print("")
print("living expenses, from the join")
living = queried_int(db, "select sum(cents) from entry join account on account.name = entry.account where account.kind = 'living'")?
mine_living: i64 @= 0
for e in entry.book()
if entry.kind_of(e.account, entry.accounts())? == "living"
mine_living @ mine_living + e.amount.cents
print(" ", entry.shown(entry.Amount(cents: living)), " agree ", verdict(living == mine_living))
return ok()
# The balances SQLite computes, in the same order this program's own
# `balances` produces — `order by` in the query, because a database's row
# order is no more promised than a map's key order.
function queried_balances(db: sqlite.Db) -> [entry.Balance]?
statement: sqlite.Statement @= sqlite.prepared(db, "select account, count(*), sum(cents) from entry group by account order by account")?
out: [entry.Balance] @= []
going: bool @= true
while going
match sqlite.stepped(statement)?
.stepped_row =>
name = sqlite.text_of(sqlite.cell(statement: statement, column: 0)?)?
count = sqlite.integer_of(sqlite.cell(statement: statement, column: 1)?)?
cents = sqlite.integer_of(sqlite.cell(statement: statement, column: 2)?)?
out @ out.push(entry.Balance(account: name, entries: count, total: entry.Amount(cents: cents)))
.stepped_done => going @ false
_ = sqlite.finalized(@statement)
return ok(out)
# One integer from one row — through the typed cell reader, so a query
# edited to return text does not answer zero.
function queried_int(db: sqlite.Db, sql: str) -> i64?
statement: sqlite.Statement @= sqlite.prepared(db, sql)?
value: i64 @= 0
found: bool @= false
match sqlite.stepped(statement)?
.stepped_row =>
value @ sqlite.integer_of(sqlite.cell(statement: statement, column: 0)?)?
found @ true
.stepped_done => found @ false
_ = sqlite.finalized(@statement)
if !found
return fail(code: "no_row", msg: sql + " answered no rows")
return ok(value)
function queried_float(db: sqlite.Db, sql: str) -> f64?
statement: sqlite.Statement @= sqlite.prepared(db, sql)?
value: f64 @= 0.0
found: bool @= false
match sqlite.stepped(statement)?
.stepped_row =>
match sqlite.cell(statement: statement, column: 0)?
.float_cell f => value @ f.value
.integer_cell i => value @ to_f64(i.value)
.text_cell => value @ value
.null_cell => value @ value
.blob_cell => value @ value
found @ true
.stepped_done => found @ false
_ = sqlite.finalized(@statement)
if !found
return fail(code: "no_row", msg: sql + " answered no rows")
return ok(value)
# Whether two balance lists are the same, account for account. Written out
# rather than `==` on the arrays, so a failure can say which account
# disagreed if this ever fires.
function same_balances(from_db: [entry.Balance], mine: [entry.Balance]) -> bool
if from_db.len() != mine.len()
return false
at: i64 @= 0
while at < mine.len()
if from_db[at].account != mine[at].account
return false
if from_db[at].entries != mine[at].entries
return false
if from_db[at].total.cents != mine[at].total.cents
return false
at @ at + 1
return true
# Two floats within a hundredth of a cent. A tolerance and not `==`,
# because SQLite's `avg` divides in binary floating point and so does the
# line beside it, and asking those to be bit-identical is asking for a
# flaky program rather than a correct one.
function near(a: f64, b: f64) -> bool
d = a - b
if d < 0.0
return 0.0 - d < 0.01
return d < 0.01
function verdict(holds: bool) -> str
if holds
return "yes"
return "no"
test "the book goes into the database and comes back unchanged"
db: sqlite.Db @= sqlite.opened().must()
build(db).must()
from_db = queried_balances(db).must()
mine = entry.balances(entry.book())
assert same_balances(from_db: from_db, mine: mine)
_ = sqlite.closed(@db)
test "sqlite's total and heroes' total are the same number"
db: sqlite.Db @= sqlite.opened().must()
build(db).must()
assert queried_int(db, "select sum(cents) from entry").must() == entry.total(entry.book()).cents
assert queried_int(db, "select count(*) from entry").must() == entry.book().len()
_ = sqlite.closed(@db)
test "the join agrees with the same join done in Heroes"
db: sqlite.Db @= sqlite.opened().must()
build(db).must()
living = queried_int(
db,
"select sum(cents) from entry join account on account.name = entry.account where account.kind = 'living'"
).must()
mine: i64 @= 0
for e in entry.book()
if entry.kind_of(e.account, entry.accounts()).must() == "living"
mine @ mine + e.amount.cents
assert living == mine
_ = sqlite.closed(@db)
test "a statement the database refuses is a refusal here, with sqlite's own words"
db: sqlite.Db @= sqlite.opened().must()
bad = sqlite.run(db, "select * from nothing_at_all")
assert bad.is_err()
assert lines.holds(text: err_text_of(bad), needle: "no such table")
_ = sqlite.closed(@db)
test "a column read at the wrong type is a refusal and not a zero"
db: sqlite.Db @= sqlite.opened().must()
build(db).must()
statement: sqlite.Statement @= sqlite.prepared(db, "select memo from entry where id = 1").must()
_ = sqlite.stepped(statement).must()
cell = sqlite.cell(statement: statement, column: 0).must()
assert sqlite.text_of(cell).must() == "september"
assert sqlite.integer_of(cell).is_err()
_ = sqlite.finalized(@statement)
_ = sqlite.closed(@db)
test "the prepared statement really is reused: ten entries, one statement"
db: sqlite.Db @= sqlite.opened().must()
build(db).must()
# `changes` is SQLite's own counter for the last statement, so ten
# inserts through one prepared statement leave it at one — which is
# what says the statement was reset and reused rather than re-prepared.
assert sqlite.changed(db) == 1
assert queried_int(db, "select count(*) from entry").must() == 10
_ = sqlite.closed(@db)
# The message of a failed call, one function per result type — because a
# generic `err_text<T>(x: T?)` is a shape this language does not have:
# generics are on functions with no constraints, and `.err e` needs the
# match to know the T? it is looking at.
function err_text_of(got: ()?) -> str
return match got
.ok _ => ""
.err e => e.msg
function why_open(got: sqlite.Db?) -> str
return match got
.ok _ => ""
.err e => e.msg
book/entry.hero · 209 righe
# What a ledger holds, and the arithmetic that must not be a float
# (spec § Types, § Failure).
#
# Corpus material (CLAUDE.md §9), M-corpus-depth. **This module has no
# `extern` in it and that is the design.** `db/sqlite.hero` is the only file
# that touches C; everything about *what the numbers mean* lives here, where
# a test can reach it without a database. It is the same split
# `examples/todo/` makes for the disk and for the same reason: a program
# whose logic can only be tested through its I/O is a program whose logic is
# not tested.
#
# **MONEY IS AN INTEGER NUMBER OF CENTS AND NEVER AN `f64`.** The reason is
# older than this language and this program states it rather than assuming
# the reader knows: `0.1 + 0.2` is not `0.3` in binary floating point, and a
# ledger that adds a thousand of those and compares the total to a figure
# somebody typed will disagree with them by a cent and be unable to say why.
# So `Amount` carries cents, the database column is an INTEGER, and the only
# float in this program is the one SQLite's `avg()` hands back — which is
# compared with a tolerance, and the comparison says so.
record Amount
cents: i64
# An amount from whole units and cents, refusing the shapes that would
# silently become a different number.
function amount(units: i64, cents: i64) -> Amount?
if cents < 0 || cents > 99
return fail(code: "bad_cents", msg: "cents are 0 to 99, not " + cents.to_str())
if units < 0
return fail(code: "negative_units", msg: "build a negative amount by negating a positive one")
return ok(Amount(cents: units * 100 + cents))
function negated(a: Amount) -> Amount
return Amount(cents: 0 - a.cents)
function added(a: Amount, b: Amount) -> Amount
return Amount(cents: a.cents + b.cents)
# `-12.34`, and the sign is written once. The whole-and-remainder split is
# taken on the ABSOLUTE value, because `-1234 / 100` truncates toward zero
# to `-12` and `-1234 % 100` is `-34` (spec § Failure), so a naive rendering
# gives `-12.-34`.
function shown(a: Amount) -> str
size: i64 @= a.cents
if size < 0
size @ 0 - size
whole = size / 100
rest = size % 100
tail: str @= rest.to_str()
if rest < 10
tail @ "0" + tail
text = whole.to_str() + "." + tail
if a.cents < 0
return "-" + text
return text
# One line of the book: which account, what it was for, how much.
record Entry
id: i64
account: str
memo: str
amount: Amount
# An account and what it holds — what a `group by` produces, and what this
# program checks SQLite's own aggregate against.
record Balance
account: str
entries: i64
total: Amount
# The entries this program writes. Written down rather than generated,
# because a ledger's whole point is that somebody can read the book and
# check the totals by hand — which is exactly what the tests below do.
function book() -> [Entry]
return [
Entry(id: 1, account: "rent", memo: "september", amount: Amount(cents: 0 - 120000))
Entry(id: 2, account: "salary", memo: "september", amount: Amount(cents: 310000))
Entry(id: 3, account: "food", memo: "market", amount: Amount(cents: 0 - 4250))
Entry(id: 4, account: "food", memo: "bakery", amount: Amount(cents: 0 - 780))
Entry(id: 5, account: "books", memo: "two paperbacks", amount: Amount(cents: 0 - 2495))
Entry(id: 6, account: "salary", memo: "a lesson", amount: Amount(cents: 8000))
Entry(id: 7, account: "food", memo: "market", amount: Amount(cents: 0 - 3110))
Entry(id: 8, account: "rent", memo: "deposit back", amount: Amount(cents: 60000))
Entry(id: 9, account: "books", memo: "a dictionary", amount: Amount(cents: 0 - 5500))
Entry(id: 10, account: "food", memo: "market", amount: Amount(cents: 0 - 2940))
]
# The accounts, and what each is for. The second table, so the program has
# a join to make rather than a join to describe.
record Account
name: str
kind: str
function accounts() -> [Account]
return [
Account(name: "rent", kind: "housing")
Account(name: "salary", kind: "income")
Account(name: "food", kind: "living")
Account(name: "books", kind: "living")
]
# **The balances, computed in Heroes.** This is one half of the check the
# whole program exists for: SQLite computes the same thing with
# `sum(amount) group by account`, and the two must agree entry for entry.
# Neither is the oracle — there is no published answer for a book somebody
# invented — so the agreement of two routes that share no line is the
# strongest claim available, and it is stronger than either alone.
function balances(entries: [Entry]) -> [Balance]
names: [str] @= []
totals: {str: i64} @= {}
counts: {str: i64} @= {}
for e in entries
seen = totals[e.account]
if seen.is_err()
names @ names.push(e.account)
totals[e.account] @ e.amount.cents
counts[e.account] @ 1
else
totals[e.account] @ seen.must() + e.amount.cents
counts[e.account] @ counts[e.account].must() + 1
out: [Balance] @= []
# ORDER: by account name, because `keys(m)` gives no order (spec
# § Bindings) and this list is printed and compared line by line.
for name in names.sort()
out @ out.push(
Balance(account: name, entries: counts[name].must(), total: Amount(cents: totals[name].must()))
)
return out
# What the whole book comes to.
function total(entries: [Entry]) -> Amount
sum: Amount @= Amount(cents: 0)
for e in entries
sum @ added(a: sum, b: e.amount)
return sum
# The kind an account belongs to, which is what the join is for.
function kind_of(name: str, all_accounts: [Account]) -> str?
for a in all_accounts
if a.name == name
return ok(a.kind)
return fail(code: "unknown_account", msg: "no account is named " + name)
test "an amount is cents, and the shapes that would lose money are refused"
assert amount(units: 12, cents: 34).must().cents == 1234
assert amount(units: 0, cents: 5).must().cents == 5
assert amount(units: 12, cents: 100).is_err()
assert amount(units: 12, cents: 0 - 1).is_err()
assert amount(units: 0 - 1, cents: 0).is_err()
test "a negative amount prints its sign once and its cents in full"
assert shown(Amount(cents: 0 - 1234)) == "-12.34"
assert shown(Amount(cents: 1234)) == "12.34"
assert shown(Amount(cents: 0 - 5)) == "-0.05"
assert shown(Amount(cents: 0)) == "0.00"
assert shown(Amount(cents: 100)) == "1.00"
# The one a float would get wrong, and the one truncation toward zero
# would print as `-12.-34` if the split were taken on the signed value.
assert shown(negated(Amount(cents: 1234))) == "-12.34"
test "the book's total is what adding the ten lines by hand gives"
# -120000 +310000 -4250 -780 -2495 +8000 -3110 +60000 -5500 -2940
assert total(book()).cents == 238925
assert shown(total(book())) == "2389.25"
test "the balances are the four accounts, in name order, with the right totals"
b = balances(book())
assert b.len() == 4
assert b[0].account == "books"
assert b[1].account == "food"
assert b[2].account == "rent"
assert b[3].account == "salary"
# Checked by hand from the ten lines above, which is what makes this a
# second opinion rather than a restatement of the code.
assert b[0].total.cents == 0 - 7995
assert b[1].total.cents == 0 - 11080
assert b[2].total.cents == 0 - 60000
assert b[3].total.cents == 318000
assert b[0].entries == 2
assert b[1].entries == 4
test "the balances add up to the book's total"
sum: i64 @= 0
for b in balances(book())
sum @ sum + b.total.cents
assert sum == total(book()).cents
test "every account in the book is one the account table names"
for e in book()
assert !kind_of(e.account, accounts()).is_err()
assert kind_of("nowhere", accounts()).is_err()
assert kind_of("food", accounts()).must() == "living"
db/sqlite.hero · 406 righe
# SQLite, bound at the width of a real program (spec § FFI; design.md §4.19).
#
# Corpus material (CLAUDE.md §9), M-corpus-depth's third family. **The
# corpus binds SQLite twice and the two programs ask different questions.**
# `examples/sqlite/` is §4.19's own acceptance — open, one statement, one
# integer back, eight functions — and it answers *does the architecture
# work at all*. This one answers *does it hold up when a program leans on
# it*: prepared statements reused across rows, values bound in, values of
# three types read out, a transaction, a join, and the error message the
# library itself produces when something is wrong.
#
# **Every signature here is checked against the SDK's `sqlite3.h` by
# clang**, which is the whole point of the group: a wrong width, a wrong
# result type or a name the header does not have is a compile error on the
# `.hero` line that wrote it, not a crash later.
#
# THE TWO SHAPES WORTH READING BEFORE THE LIST:
#
# - `sqlite3_bind_text`'s last parameter is a **destructor**, and it is the
# argument that decides how long SQLite keeps the bytes: `SQLITE_STATIC`,
# which is `nullptr`, means *keep the caller's bytes*, and
# `SQLITE_TRANSIENT` means *copy them before returning*. **This program
# passes `SQLITE_TRANSIENT`**, so there is no lifetime to reason about at
# all: the copy happens inside the call. Until 2026-09-09 it passed `nullptr`
# with eleven lines above it explaining why that was safe, and panel 124
# measured that the explanation was subtly wrong — it named the frame, and
# the thing actually keeping the bytes alive was the refcount of a record
# field the loop variable owned. Both spellings are `const char *` in the
# header, so **nothing about the Heroes side can tell them apart**: the fact
# lives in argument five, which is why clang can check it and a rule about
# Heroes cannot — and why, since panel 171, the `text` parameter carries no
# `lent` and `bind_text` hands the bytes over as a lease it releases itself,
# where the other three string parameters of this group are marked.
# - `sqlite3_column_text` answers `const unsigned char *`, which is a
# `cstr` here, and a `cstr` becomes a `str` only through `validated` —
# which can fail, because the bytes are the database's and not this
# program's (spec § Types). `db/rows.hero` is where that `str?` is
# handled rather than assumed away.
extern "sqlite3.h" link "sqlite3"
# Result codes and column types, read from the header rather than
# written as numbers (M-header-constants): a typo is
# `error[unknown_name]` locally, and a wrong VALUE is impossible
# because there is no value here to get wrong.
constant SQLITE_OK: i64
constant SQLITE_ROW: i64
constant SQLITE_DONE: i64
constant SQLITE_INTEGER: i64
constant SQLITE_FLOAT: i64
constant SQLITE_TEXT: i64
constant SQLITE_NULL: i64
# `((sqlite3_destructor_type)-1)` in the header, which is a cast of -1 to
# a function pointer, so it is a `ptr` here and the group's own two
# assertions check it: `HERO_RET_PTR` on the type and
# `__builtin_constant_p` on it being a value rather than an object.
constant SQLITE_TRANSIENT: ptr
# The two HANDLES, since 2026-09-13 (panel 145, defect 029). A `record`
# inside a group with a `tag` and NO fields is a pointer to a type the
# header names and leaves opaque: `CDb` is C's `sqlite3 *` and `CStmt` is
# `sqlite3_stmt *`. The two wrapper records below kept two Heroes types
# over one `ptr` by hand, at thirteen `.handle` unwraps and with the
# binding's own interior unprotected; the handles now carry that inside
# the group, where clang checks the names against the header too.
record CDb tag sqlite3
record CStmt tag sqlite3_stmt
# **The two ends of a handle's life, since 2026-09-14** (panel 148). This is
# the file the sitting was decided against: 22 of the 23 escaping paths the
# census counted acquire inside THIS module's wrappers, one module away from
# every place the rest of the program holds a handle. The mark therefore
# goes on the CALL that creates the obligation and propagates outward, the
# way `consumes` did — not on the TYPE, which cannot know whether a given
# call gives or lends.
#
# `sqlite3_next_stmt` and `sqlite3_db_handle` are the counter-examples and
# this binding declares neither: both hand back a handle SQLite keeps, and
# the day one of them is bound it says `borrows` rather than nothing.
# `lent` on `filename` and on the two `sql` parameters: SQLite reads the
# string during the call and copies what it keeps, which the ffi seat of
# panel 171 measured by handing each a freed argument under the sanitizer.
# Without the word the compiler assumes C keeps the pointer and refuses
# the lend (spec § 13). `sqlite3_bind_text` below carries no word, and
# `bind_text` says why.
function sqlite3_open(filename: cstr lent, @out: CDb acquires sqlite3_close) -> i64
function sqlite3_close(db: CDb consumes) -> i64
# **The fifth argument is `char **errmsg`, and this program asks for it
# again** — panel 109's condition 8, the program the whole milestone was
# convened for. A non-NULL one makes SQLite allocate a copy of the message
# that the CALLER owns and must release with `sqlite3_free`, and `owned
# sqlite3_free` is how the declaration says so: the compiler copies the
# bytes out, calls `sqlite3_free` by name, and hands the program a `str?`.
# A call of `sqlite3_free` from this file would now be
# `error[owned_freer_called]`, because the compiler is already making it.
#
# **THE HISTORY IS KEPT BECAUSE IT IS THE ARGUMENT.** This was an `@error:
# ptr` until it was repaired: the program asked for the copy, never freed it and
# never even read it, so every refused statement leaked 40 bytes — found by
# the Linux leg of CI under `--sanitize`, because LeakSanitizer does not
# exist on Darwin arm64 (CLAUDE.md §7). The repair that day was to stop
# asking, and it was the right repair on that day, for the reason panel 109
# then measured three ways: **a caller-owned C string could be freed or
# read, never both**, so the program that reads the message and frees it
# could not be written in this language at all. It can now, and this is it.
function sqlite3_exec(db: CDb, sql: cstr lent, callback: ptr, context: ptr, @error: cstr owned sqlite3_free) -> i64
# The freer the mark names. It is declared and never called: calling it is
# a compile error precisely because the compiler already does.
function sqlite3_free(p: ptr)
function sqlite3_errmsg(db: CDb) -> cstr
function sqlite3_changes(db: CDb) -> i32
function sqlite3_prepare_v2(db: CDb, sql: cstr lent, length: i32, @statement: CStmt acquires sqlite3_finalize, @tail: cstr) -> i64
function sqlite3_step(statement: CStmt) -> i64
function sqlite3_reset(statement: CStmt) -> i64
function sqlite3_finalize(statement: CStmt consumes) -> i64
function sqlite3_bind_int64(statement: CStmt, column: i32, value: i64) -> i64
function sqlite3_bind_double(statement: CStmt, column: i32, value: f64) -> i64
function sqlite3_bind_text(statement: CStmt, column: i32, text: cstr, length: i32, destructor: ptr) -> i64
function sqlite3_column_count(statement: CStmt) -> i32
function sqlite3_column_type(statement: CStmt, column: i32) -> i32
function sqlite3_column_int64(statement: CStmt, column: i32) -> i64
function sqlite3_column_double(statement: CStmt, column: i32) -> f64
function sqlite3_column_text(statement: CStmt, column: i32) -> cstr
# Eighteen functions and seven constants. The count is here because the
# milestone's plan asked for **at least fifteen bound functions** — the
# measured gap was that every FFI program in this corpus was 65 to 192
# lines and bound a handful — and a number in a plan is worth checking
# against the thing it produced. `grep -c '^ function' db/sqlite.hero`
# answers it without trusting this sentence.
#
# **And it did not, until somebody ran it.** This line has said *eighteen* since
# the file was written and the answer was **17**; `sqlite3_free` arriving with
# the `owned` mark is what made the sentence true, by accident, on the day
# somebody finally ran the command it names. That is CLAUDE.md §1 in one file:
# a count in prose is a claim, the command beside it is the instrument, and a
# claim nobody runs is wrong for as long as nobody runs it.
# Whether a prepared statement's column holds text, an integer, a float or
# nothing. A `variant` and not the raw `i32`, so the reader below cannot
# forget a case: SQLite has five column types and a program that handles
# four of them silently reads the fifth as a zero.
variant Cell
integer_cell
value: i64
float_cell
value: f64
text_cell
value: str
null_cell
# The one SQLite has and this program does not read: a BLOB. It is a
# case rather than an omission, so `match` forces every reader to say
# what it does with one, and this program says "refuse" rather than
# "treat as empty text".
blob_cell
# What a column holds, read at its own type. **The type is asked rather
# than assumed**: `sqlite3_column_int64` on a text column answers 0 and
# says nothing, which is the silent wrong answer this whole corpus exists
# to catch.
function cell_at(statement: CStmt, column: i32) -> Cell?
kind = sqlite3_column_type(statement: statement, column: column)
if to_i64(kind).must() == SQLITE_INTEGER
return ok(.integer_cell(value: sqlite3_column_int64(statement: statement, column: column)))
if to_i64(kind).must() == SQLITE_FLOAT
return ok(.float_cell(value: sqlite3_column_double(statement: statement, column: column)))
if to_i64(kind).must() == SQLITE_TEXT
# The bytes are the database's. `validated` copies them into a
# Heroes `str` and refuses what is not UTF-8, which is a thing a
# database can hold and this program must not print blindly.
text = sqlite3_column_text(statement: statement, column: column).validated()
if text.is_err()
return fail(
code: "not_text",
msg: "column " + to_i64(column).must().to_str() + " holds bytes that are not UTF-8"
)
return ok(.text_cell(value: text.must()))
if to_i64(kind).must() == SQLITE_NULL
return ok(.null_cell)
return ok(.blob_cell)
## The wrappers, and the rule that forces them
# **AN `extern` IS NOT CALLABLE ACROSS A MODULE BOUNDARY**, and this program
# learned it from the compiler on its first run:
#
# error[extern_across_modules]: `sqlite3_open` is an `extern` of module
# `db/sqlite` — an extern is never callable across a module boundary,
# because only `db/sqlite` carries the header that checks it
# note: §4.19: write a Heroes function beside the `extern` and call that
#
# The reason is the whole architecture in one line: clang checks a signature
# against `sqlite3.h`, and the header is `#include`d in the C of THIS module
# only. A caller in another module would be a call nothing verified. So the
# boundary is drawn here, on purpose: everything below is a Heroes function
# with a Heroes signature, and the rest of the program never sees a `cstr`,
# a `ptr` result code or a column index counted from one.
#
# That is also why this file is the only one with `link "sqlite3"` in it,
# and why a machine without the library skips exactly this program rather
# than half of it.
# **A `ptr` MAY NOT BE THE ELEMENT OF A `T?`, and this program met that on
# its first run** — which is why a handle here is a record with one field
# rather than a bare pointer:
#
# unsupported[pointer_element]: `ptr` as the element of a `T?` is not
# emitted yet
# note: hold the pointer in a `record` and make an array of that instead
#
# The diagnostic is a declared gap rather than a defect (§4.16's shape: the
# backend says what it does not emit), and its note is the repair. But it
# lands squarely on the FFI, where §4.19 asks for *complete and bug-proof*:
# a binding that opens something is the commonest shape there is, and
# `open() -> ptr?` is how anybody writes it first. The wrapping is one line
# and it also improves the signature — `Db` and `Statement` are two types
# the compiler will not let a caller confuse, where two `ptr`s are one type
# — so the program keeps the records and the finding is filed rather than
# argued here.
record Db
handle: CDb
record Statement
handle: CStmt
# A database, opened in memory. `:memory:` because a corpus program that
# wrote a file would have to clean it up, and its output would depend on
# what a previous run left behind.
function opened() -> Db?
db: CDb @= nullptr
if sqlite3_open(":memory:".cstr(), @db) != SQLITE_OK
# **A FAILED OPEN STILL HANDS BACK A CONNECTION, and dropping it leaks
# something far larger than a message.** This branch is the shape next
# to the leak `run` had, attacked before the repair was committed
# because CLAUDE.md §1 says the provoking case is a witness and not the
# class. Measured on both platforms rather than read off the
# documentation, sqlite 3.51.0 here and 3.46.1 in the Linux image:
# `sqlite3_open("/no-such-directory-here/x.db", &db)` answers **14**
# with `db` **non-NULL**, `sqlite3_errmsg` on that handle says `unable
# to open database file`, and `sqlite3_close` on it answers 0. So the
# handle is this program's to release here too — and the reason is
# SQLite's own, read off the handle before it is closed, rather than the
# sentence this program used to invent about a failure it had not
# actually asked about.
reason = why(Db(handle: db))
_ = sqlite3_close(db)
return fail(code: "cannot_open", msg: reason)
return ok(Db(handle: db))
function closed(@db: Db) -> i64
return sqlite3_close(db.handle)
# One statement run for its effect, with SQLite's own message on failure.
#
# **THIS FUNCTION LEAKED 40 BYTES PER REFUSED STATEMENT, and
# only one of the three platforms could see it.** It passed `@error` to
# `sqlite3_exec`, which allocates a copy of the message for the caller to free;
# nothing freed it, and nothing read it either. What found it is the Linux leg
# of CI under `--sanitize`, because **LeakSanitizer does not exist on Darwin
# arm64** (CLAUDE.md §7) — so the program ran clean on the machine it was
# written on, in all three configurations, while leaking on every failure.
#
# **The first repair was to stop asking; the repair now is to ask and be
# given it**, which is a different thing and a better one. `owned
# sqlite3_free` on the declaration makes the cell a `str?` the compiler has
# already copied and already freed, so the message below is SQLite's own words
# about *this statement* rather than the connection's last error — and there
# is no rule left for anybody to remember.
#
# `why(db)` stays as the fallback rather than being deleted, and that is not
# belt and braces: the cell is null when SQLite chooses not to fill it, and a
# refusal with an empty reason is the shape this program exists to refuse.
function run(db: Db, sql: str) -> ()?
problem: str? @= fail(code: "none", msg: "sqlite has not answered yet")
if sqlite3_exec(db: db.handle, sql: sql.cstr(), callback: nullptr, context: nullptr, error: @problem) != SQLITE_OK
return fail(code: "statement_refused", msg: sql + ": " + problem.default(why(db)))
return ok()
# How many rows the last statement changed — SQLite's own counter, which is
# the second opinion this program checks its own inserts against.
function changed(db: Db) -> i64
return to_i64(sqlite3_changes(db.handle)).must()
# A prepared statement, which is the shape that makes this program different
# from `examples/sqlite/`: prepared once, bound and stepped many times.
function prepared(db: Db, sql: str) -> Statement?
statement: CStmt @= nullptr
tail: cstr @= nullptr
if sqlite3_prepare_v2(db: db.handle, sql: sql.cstr(), length: -1, statement: @statement, tail: @tail) != SQLITE_OK
return fail(code: "cannot_prepare", msg: sql + ": " + why(db))
return ok(Statement(handle: statement))
function finalized(@statement: Statement) -> i64
return sqlite3_finalize(statement.handle)
# Ready to be bound and stepped again. The whole reason a prepared
# statement is worth having.
function reset(statement: Statement) -> ()?
if sqlite3_reset(statement.handle) != SQLITE_OK
return fail(code: "cannot_reset", msg: "sqlite would not reset the statement")
return ok()
# One step. `.stepped_row` when a row is there, `.stepped_done` at the end,
# and a refusal otherwise — a variant rather than the raw code, so a caller
# cannot compare against the wrong constant.
#
# `stepped` took its statement `@` from 2026-09-13 (panel 139, defect 030) to
# 2026-10-11, to say that a step advances the cursor every copy of this record
# reaches. The marker changed nothing in C, the handle being a copied address
# either way, and spec § 3 says it in words: a function taking a `ptr` or a
# handle without `@` may still change what C holds. Since panel 210 an `@`
# parameter nothing writes or ends is refused (spec § 5), so the promise lives
# in that sentence and the signature takes the statement as its twelve
# by-value siblings do.
variant Step
stepped_row
stepped_done
function stepped(statement: Statement) -> Step?
code = sqlite3_step(statement.handle)
if code == SQLITE_ROW
return ok(.stepped_row)
if code == SQLITE_DONE
return ok(.stepped_done)
return fail(code: "step_refused", msg: "sqlite refused the step with code " + code.to_str())
# Binding, one function per type this program uses. The column index is
# ONE-BASED in SQLite and this is the only place that knows it: every
# caller counts from one because the wrapper says `at:` and the doc says
# what `at` means, which is cheaper than a translation nobody remembers.
function bind_int(statement: Statement, at: i64, value: i64) -> ()?
if sqlite3_bind_int64(statement: statement.handle, column: to_i32(at).must(), value: value) != SQLITE_OK
return fail(code: "cannot_bind", msg: "sqlite refused an integer at " + at.to_str())
return ok()
function bind_float(statement: Statement, at: i64, value: f64) -> ()?
if sqlite3_bind_double(statement: statement.handle, column: to_i32(at).must(), value: value) != SQLITE_OK
return fail(code: "cannot_bind", msg: "sqlite refused a float at " + at.to_str())
return ok()
# `sqlite3_bind_text` keeps or copies by its FIFTH argument, so no one word is
# true of its `text` parameter and the declaration above carries none (panel
# 171): with `SQLITE_STATIC` it keeps the pointer, with `SQLITE_TRANSIENT` it
# copies before returning. An unmarked parameter is assumed to keep, so a lend
# is refused there and the bytes go over as a LEASE, a copy this function owns
# and releases the moment the call is back. `SQLITE_TRANSIENT` makes that
# release safe: SQLite has its own copy by then, so a rearrangement that moves
# the `step` cannot break it (panel 124, ratified 2026-09-09).
function bind_text(statement: Statement, at: i64, text: str) -> ()?
held: cstr @= text.lease()
rc = sqlite3_bind_text(
statement: statement.handle,
column: to_i32(at).must(),
text: held,
length: -1,
destructor: SQLITE_TRANSIENT
)
end_lease(@held)
if rc != SQLITE_OK
return fail(code: "cannot_bind", msg: "sqlite refused text at " + at.to_str())
return ok()
# How many columns the statement's result has — asked rather than assumed,
# so a query edited to select one more column does not read past the end.
function columns(statement: Statement) -> i64
return to_i64(sqlite3_column_count(statement.handle)).must()
# One column of the current row, at its own type. Zero-based here, because
# SQLite's column READERS are zero-based while its binders are one-based —
# a genuine wart of that library, and the wrapper keeps it visible in the
# names (`at:` binds from one, `column:` reads from zero) rather than
# papering over it.
function cell(statement: Statement, column: i64) -> Cell?
return cell_at(statement: statement.handle, column: to_i32(column).must())
# A cell as the integer it is, or a refusal naming what it was instead.
# Every caller of this wants a number and would otherwise get a zero.
function integer_of(c: Cell) -> i64?
return match c
.integer_cell i => ok(i.value)
.float_cell => fail(code: "wrong_type", msg: "the column holds a float where a whole number was asked for")
.text_cell => fail(code: "wrong_type", msg: "the column holds text where a whole number was asked for")
.null_cell => fail(code: "wrong_type", msg: "the column is null where a whole number was asked for")
.blob_cell => fail(code: "wrong_type", msg: "the column holds a blob, which this program does not read")
function text_of(c: Cell) -> str?
return match c
.text_cell t => ok(t.value)
.integer_cell i => ok(i.value.to_str())
.float_cell f => ok(f.value.to_str())
.null_cell => fail(code: "wrong_type", msg: "the column is null where text was asked for")
.blob_cell => fail(code: "wrong_type", msg: "the column holds a blob, which this program does not read")
# The library's own message for the last thing that went wrong. Bound
# because a program at this scale has to be able to say WHY a statement
# was refused, and SQLite is the only thing that knows.
function why(db: Db) -> str
return sqlite3_errmsg(db.handle).validated().default("sqlite said nothing")
report/lines.hero · 83 righe
# The report's text, and nothing else (spec § Strings, arrays, maps).
#
# Corpus material (CLAUDE.md §9), M-corpus-depth. Here for the reason
# `examples/todo/` gives for its own split: every decision about *what the
# answer is* lives in `book/entry.hero` and in the queries, so the tests
# that check the arithmetic never have to read text, and the tests that
# check the text never have to open a database.
use book/entry
constant BALANCE_HEADING: str
"account kind entries total"
# One line of the book: the entry's own fields, and the account's kind
# fetched through the join this program also asks the database to do.
function book_lines(entries: [entry.Entry], accounts: [entry.Account]) -> [str]
out: [str] @= []
for e in entries
kind = entry.kind_of(e.account, accounts).default("?")
out @ out.push(
" " + wide(text: e.id.to_str(), to: 3) + wide(text: e.account, to: 9) + wide(text: kind, to: 9) + wide(text: e.memo, to: 17) + right(text: entry.shown(e.amount), to: 10)
)
return out
function balance_line(b: entry.Balance, kind: str) -> str
return wide(text: b.account, to: 9) + wide(text: kind, to: 9) + right(text: b.entries.to_str(), to: 7) + right(text: entry.shown(b.total), to: 11)
# Padded on the right, never truncated: a report that cuts a value to fit
# shows the wrong value.
function wide(text: str, to: i64) -> str
if text.len() >= to
return text + " "
return text + repeat(" ", to_u64(to - text.len()).must())
# Padded on the LEFT, which is what a column of numbers wants: the digits
# line up under each other and a longer number pushes the column rather
# than hiding in it.
function right(text: str, to: i64) -> str
if text.len() >= to
return " " + text
return repeat(" ", to_u64(to - text.len()).must()) + text
# Whether `text` holds `needle`. Here because `main.hero` asserts against
# SQLite's own error message, and a message is the one thing this program
# does not control the exact words of.
function holds(text: str, needle: str) -> bool
if needle.len() > text.len()
return false
at: i64 @= 0
while at + needle.len() <= text.len()
if text.slice(from: at, to: at + needle.len()) == needle
return true
at @ at + 1
return false
test "a cell is padded and never cut, on both sides"
assert wide(text: "ab", to: 5) == "ab "
assert wide(text: "abcdef", to: 3) == "abcdef "
assert right(text: "7", to: 4) == " 7"
assert right(text: "1234567", to: 4) == " 1234567"
test "a book line carries the entry, its account's kind and the amount"
line = book_lines(entry.book(), entry.accounts())[0]
assert holds(text: line, needle: "rent")
assert holds(text: line, needle: "housing")
assert holds(text: line, needle: "september")
assert holds(text: line, needle: "-1200.00")
test "a balance line carries the account and its total"
b = entry.balances(entry.book())[1]
line = balance_line(b, "living")
assert holds(text: line, needle: "food")
assert holds(text: line, needle: "living")
assert holds(text: line, needle: "-110.80")
test "the search finds what is there and refuses what is not"
assert holds(text: "no such table: nothing", needle: "no such table")
assert !holds(text: "short", needle: "much longer than the text")
assert holds(text: "abc", needle: "abc")
impronta sha256 5f01ef9f6828 · 5 file · index.json
Successivo: curl. Tutti gli esempi. ← Precedente: sqlite
Eseguine uno: i quattro comandi. Impara il linguaggio, oppure leggi la specifica completa in un solo file.