LeanDB 0.5.0

Portable domain models, typed read and transaction programs, and the
LDB-12 through LDB-24 engine improvements. Lean remains at 4.33.0;
leansqlite is unchanged and leanontology is pinned to
322a4c12631dd8ece6ae9841a5e6b630d08d1e3b.

• Portable model. LeanDb.Model describes entities, checked value
  types, unique and cascade constraints, links, Changes, and DB /
  Query programs without importing SQLite. The same programs run in
  memory and on SQLite through LeanDb.Native, native_schema%, and
  derive_requirements. Structured and represented values can occupy
  one column. The domain bridge also checks native storage evidence and
  typed migration requirements.

• Typed API. The typed layer provides schema-indexed queries, validated
  reads, typed write errors, and transaction programs with a pure meaning.
  Differential tests compare that meaning with SQLite execution; the
  preservation laws and their remaining gaps are documented in
  the typed interface guide.

• Reliability. HTTP dispatch and host handshakes are bounded; hosted
  child processes are cleaned up on failure. Restore respects writer
  locks, migration errors restore connection settings, custom migration
  steps cannot escape the engine transaction, and backup names avoid
  collisions. MCP validates arguments and does not reply to notifications.
  Seeding refuses a non-empty catalog unless forced; scaffolding and
  import generation validate and escape names and preserve existing files.

• Packaging. Example and benchmark lockfiles include the pinned
  leanontology dependency. The engine, portable model, and SQLite model
  interpreter have separate Lake libraries, so precompiled client adapters
  can load the engine without undeclared model dependencies. Shared-library
  names match Lean module initializers so native model consumers also load
  their dependencies in the correct order.

• M15b3. Txn.update_wf, Txn.set_wf, Txn.append_wf: on a WF
  state, update, set and append yield a WF state whether they
  succeed or fail (HasPack, LawfulEntity). Unique keys compare with
  Unique.keyClash a b := a == b || b == a, symmetric by construction:
  Float.beq is extern, so Array Col equality is not provably
  commutative. It agrees with IEEE and SQLite (-0.0 = 0.0; SQLite has
  no NaN). patch and delete have no WF lemma yet; the remainder is
  in docs/typed-interface.md.

• M15b2. Table.nextOk (1 ≤ next ≤ natSqlMax + 1) is in Table.check.
  assign does not wrap Int64.ofNat. DbState.empty_wf.
  Txn.insert_wf: on a WF state, insert yields a WF state
  whether it succeeds or fails (HasPack, LawfulEntity). Part 1's
  Txn.denote_wf is renamed denote_wf_of_unchanged; the name
  denote_wf is reserved for the whole-program law (remainder).

• M15b. Laws LeanAPI theorems need, in LeanDb/Typed/Laws.lean.
  Exact plans are denotational (approx.denote = pred.denote when there
  is no opaque leaf). Aggregates are count = size ∘ rows,
  exists = !isEmpty ∘ rows, first = head? ∘ rows. Codecs carry
  LawfulColCodec.roundTrip and LawfulSqlOrd.order_toCol; Nat is
  bounded to natSqlMax. Reads do not write (Txn.ReadOnly). Failure
  exactness is iff against firstDuplicate / firstMissingRef in
  declaration order. Table frames (get_set_other lifted to each write)
  and query frames (denote_eq_of_admitted, including joins). Remainder
  is listed in docs/typed-interface.md.

• M15a. Meaning agrees with SQLite on the M14 review findings D1–D10.
  Child lists are in DbState.snapshot; two-level cascade already
  agreed (deleteAt); Option (Ref) is a typed FK and child-list
  Refs are refused at schema%; append CAS compares list contents
  and checks parent unique/FK; orderBy pushes SQL only for SqlOrd
  (closed enums sort in Lean); Current has a private constructor;
  Nat above Int64.max is not Checked; first after limit := 0
  is none and huge windows apply in Lean; a join keeps a left-side
  quantifier; mixed-invariant patch is SetError.invalid;
  UpdateError.stale BEq compares payloads; issued ids are positive
  (Id.toNat, Table.refsOk). LeanDb.ExecutesAsMeaning s is the
  named hypothesis for LeanAPI (not an axiom). Harness: 572 fixed-seed
  cases. Docs: docs/typed-interface.md.

• M15-pre. DbState is a lawful (t : Fin nTables) → Table (pack t).ty
  with no unsafe / implemented_by in LeanDb/Typed. get / set /
  load are the executed definitions; get_set_same, get_set_other,
  empty_rows, and insert_team_on_empty are proved. Read.get /
  lookup return Valid α (invariant proof; coerces to Stored);
  Txn.update / append take that proof plus Checked so callers need
  not re-check. deleteAt is fueled by rowCount (no partial).
  exact_plan is kernel-reducible (decide, not native_decide).
  scripts/CheckAxioms.lean allowlists propext / Classical.choice /
  Quot.sound. Harness compares production load to denote through
  lawful get.

• M15-pre (part 2). Table.rows : List (Valid α) so read evidence
  is by construction (Has.entity_eq / Table.cast). Read.first /
  all / page answer Valid α (joins Valid α × Valid β);
  Query.from stays Stored. Decode-time invariant failure is
  DbFault.corruption. deleteAt erases before walking (fuel =
  rowCount suffices on a finite cascade graph). LeanAPI writeStep's
  invariant if can be deleted: Read.first on a filtered query
  already returns Valid. TestsM14c.lean random harness: 100 cases
  covering field-subset patch, cascade delete, and exact joins.

• M14c. Close remaining QUERIES.md §3 / §5 gaps: patch writes only
  the named fields (meaning merge and SQL UPDATE); SetError lists
  only constraints over written fields (Unique.Touching /
  ForeignKey.Within reduce to Empty); window/first/count/exists
  refuse a non-exact plan at elaboration; FK join is a SQL JOIN;
  decidable DbState.checkWF (harness after every successful write);
  Runtime.Service.runRead on a reader snapshot and runTxn on the
  writer; per-FK ON DELETE RESTRICT or CASCADE (cascade%), mirrored
  in SQLite, meaning, and DeleteError.Restricting. Tests in
  TestsM14c.lean. Remaining deviations are listed in
  docs/typed-interface.md.

• M14b. Typed writes and transaction programs: schema-derived
  InsertError / UpdateError / SetError / AppendError /
  DeleteError, Txn σ s ε α with ST-style Current σ α, Txn.denote
  and Txn.run (BEGIN IMMEDIATE, SAVEPOINT per write, constraints
  checked in declaration order), and an execution-equals-meaning harness
  (LeanDb/Typed/Harness.lean, TestsM14b.lean).

• LDB-24. readSnapshot is public: a deferred BEGIN DEFERRED
  snapshot for multi-statement reads, so adapters need not rebuild one.

• LDB-23. Pred.Snapshot.rows fails on an undecodable row instead of
  dropping it (which made forall vacuously true over corrupt data).

• LDB-22. count / exists? apply the lambda, not only the plan, so
  a residual (or a hand-written .tt plan) cannot overcount. countP /
  existsP still push COUNT(*) / EXISTS for exact plans.

• LDB-21. patch refuses a guard that contains an opaque leaf.
  Opaque used to render as true, so a residual false guard still wrote.

• LDB-20. Multi-statement verbs that join an outer transaction run
  under a SAVEPOINT, so catching their error and committing cannot keep
  partial effects.

• LDB-19. Runtime.Service.withReader locks each pooled connection
  and never hands out the writer. readers := 0 still opens one
  dedicated read-only slot, so a reader cannot write and two callbacks
  cannot share one SQLite handle.

• LDB-18. Nat columns are bounded to 0 … Int64.maxValue. Writes
  of a larger Nat are .decode; a comparison bound outside that range
  renders as a tautology or contradiction instead of wrapping, so
  select (·.n < 2^64) agrees with its meaning. SqlOrd Nat stays.

• LDB-17. selectP / existsP apply LIMIT/OFFSET after the
  residual Lean filter unless the plan is exact (and not a join). A
  pushed window on the approx superset can no longer hide a later
  matching row (existsP false negatives, short pages).

• LDB-15 (#129). append old new: grow an entity's child lists against
  the value that was read. Only the added child rows are written, at the
  positions after the stored ones; the parent's columns are written under
  update's compare-and-swap. A list that moved on since the read, or a
  parent that did, is .stale, in one connection or across processes
  (BEGIN IMMEDIATE, backed by the (parent, position) UNIQUE index). A
  list that does not continue the stored one is .notAppend. update's
  docstring now says plainly that its CAS does not see child lists.

• LDB-16 (#130). Entity invariants. @[leandb_invariant] def T.invariant : T → Bool, declared before deriving instance LeanDb.Entity for T, is
  checked on every read (after the child lists are attached) and before
  every write (insert, insertMany, update, patch, append). A row
  that fails is .invariant table name: never returned, never stored. The
  attribute refuses a check declared after Entity T exists. The name is
  part of the schema: TableSpec.invariant, schema_json, the fingerprint
  (table:invariant=<name>; unchanged for a table without one), and a
  journaled restampInvariant migration step.

• Freeze (#131). Frozen snapshots are written with named fields and
  include indexes and invariant. Since 0.4.0 they were written as
  ⟨name, #[…]⟩, which does not compile against a three-field
  TableSpec. The legacy example's snapshots are updated.

• Breaking. TableSpec has a fourth field, invariant. Code that
  builds one positionally (⟨name, columns, indexes⟩) adds , none, or
  switches to named fields. New DbError constructors: invariant,
  notAppend.

• LDB-13 (#112). Runtime.snapshot runs its VACUUM INTO on a
  pooled reader connection, holding that slot's lock for the backup, so
  the writer keeps serving. snapshotOn .writer runs it on the writer
  under the admission lock, as before. The copy is written to dest.tmp
  and renamed on success, so a failed snapshot leaves no torn output. One
  snapshot runs at a time (RuntimeError.snapshotBusy), and a gated
  service is refused. restore waits for a running snapshot, which
  stands down as .snapshotAborted and removes its partial output, and
  now reopens the reader pool as well as the writer, so withReader,
  runRead and snapshots after a restore read the restored file.
  status reports the running snapshot's lane and the last one's lane,
  duration and size. RuntimeError has two new constructors,
  snapshotBusy and snapshotAborted.

• LDB-12. DbJson.via encode parse: a JSON codec for a nested type
  with proof fields, through its data representation σ — encode
  erases the proofs, parse re-decides them, and the shape the
  fingerprint, schema and migrate see is σ's. A stored value that
  fails parse decodes as DbError.decode naming the table and field.
  The derive's proof-field errors name DbJson.via as the way out.

• Custom migration steps can run verbs (#75, #117). Migration.applyOn
  counts its BEGIN … COMMIT as an open transaction, so a verb, append,
  or withTransaction inside a Step.custom nests under a SAVEPOINT
  instead of failing with cannot start a transaction within a transaction. A step that fails after its verb ran rolls the verb's
  writes back with the migration. A step that COMMITs or ROLLBACKs the
  migration's transaction away is still refused.

• LDB-14. Pushed string predicates: Pred.prefix renders
  (c LIKE ? ESCAPE '\' AND instr(c, ?) = 1) with the pattern escaped
  (\, %, _) and bound, Pred.contains renders instr(c, ?) > 0
  (byte-exact), and Pred.icontains renders
  instr(lower(c), lower(?)) > 0 — ASCII-only case folding on both
  sides. The reifier accepts String.startsWith/String.contains on a
  column, and contains with toLower on both sides; a lowered
  startsWith stays in Lean. All three are exact: LIKE folds
  ASCII case, and the instr conjunct makes prefix case-sensitive like
  startsWith, so a pushed LIMIT/OFFSET, COUNT(*) or EXISTS over
  them is sound. A negated string leaf stays in Lean.
  IndexSpec.collate := some .nocase declares a COLLATE NOCASE index,
  which is what lets SQLite serve a pushed prefix from an index; it is
  DDL, schema-JSON and fingerprint material.

Validation: ./scripts/release_check.sh passed, including the engine, DDD and model suites, precompiled consumers, examples, dashboard, scaffolding/import, and HTTP/MCP/host checks. Linux and macOS CI passed. Release versions, license, and local documentation links were checked.