LeanDB 0.5.1

• Schemas of more than fifteen entities (#139). schema%, and
  native_schema% through it, generated IsSchema.pack as a match on
  Fin literals, which Lean's match compiler rejected with "Missing
  cases" from about the sixteenth entity on. pack now indexes an array
  of the packed entities, so a schema of any size elaborates. The model
  suite declares a twenty-entity schema and writes and reads its first and
  last tables on SQLite.

Lean 4.33.0, leansqlite, and leanontology are unchanged.

Validation: ./scripts/release_check.sh passed, including the engine, DDD and model suites, precompiled consumers, examples, dashboard, scaffolding/import, and HTTP/MCP/host checks; the DDD negative fixtures were rejected as expected. Linux and macOS CI passed.

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 four...

LeanDB 0.4.0

LeanDB 0.4.0 lands the LeanGD engine surface (LDB-01 … LDB-11). Defaults stay byte-identical to 0.3.x (synchronous=FULL, 5s busy timeout, audit log .all).

• LDB-01. transaction / withTransaction / untrackedSqlite and LeanDb.Runtime.Service: BEGIN IMMEDIATE at depth 0, savepoints when nested, typed .abort, poisoned connections after a failed ROLLBACK, serialized withConnection, drain/resume/snapshot/restore/close.
• LDB-02. OpenConfig (synchronous, cache_size, mmap_size, wal_autocheckpoint, allowlisted extraPragmas) plus LEANDB_* environment overrides.
• LDB-03. Indexes α declares indexes and composite UNIQUE constraints; they appear in DDL, schema JSON, the fingerprint, and migrate add/drop plans. Child tables get (parent, position) UNIQUE.
• LDB-04. selectP takes a pushed Order and Window (LIMIT / OFFSET); a Lean-side sort plus a limit is refused. Tie-break is , id ASC.
• LDB-05. LogConfig.verbs (all / failuresAndPlans / failuresOnly / none) and sampleEvery; CLI default remains .all.
• LDB-06. count / countP / exists? / existsP push COUNT(*) / EXISTS when the predicate has no residual.
• LDB-07. Typed patch with a Pred guard; PatchResult is .updated / .notFound / .guardFailed.
• LDB-08. insertMany and keyset scan.
• LDB-09. Runtime.Config.readers and Service.withReader; write verbs on a read-only connection return DbError.readOnly.
• LDB-10. deriving instance LeanDb.ClosedEnum / DbJson / Inline works post-hoc on LeanDB-free domain types.
• LDB-11. Extra tables in a fingerprinted instance are tolerated; Base.auxiliary declares FTS5 objects; searchP binds MATCH.

Also in this release: JSON true/false only on Bool columns; colliding table names are refused; --db is taken only before the verb; WAL + deferred snapshots; HTTP Host/Origin pin and JSON Content-Type requirement; restore-safety path shared with the runtime.

Lean 4.33.0 and the pinned SQLite dependency are unchanged.

Validation: lake build LeanDb, lake build leandb, and .lake/build/bin/leandb_tests (all engine tests passed).

LeanDB 0.3.1

LeanDB 0.3.1 adds a practical documentation set and cleans up the examples.

• Read the core concepts guide, glossary, and roadmap.
• The README is shorter and includes the architecture diagram. Example READMEs replace the old CLI transcripts.
• The old proposal directory and the Gpus, Kernels, and Pricewatch examples have been removed. Release checks now cover the remaining packages.
• This release also includes the typed HTTP client integration and pinned dashboard dependency added after the 0.3.0 tag. HTTP clients use the separate leandb-http adapter.

Lean 4.33.0 and the pinned SQLite dependency are unchanged.

Validation: the full release check passed, the guide's Lean examples compile, and all 48 local documentation links resolve.