TODO.md

TODO

Suggestions from the linen v1.6.1 dependency review (2026-09-28), re-checked for the bumps to linen v1.6.2 (0.3.2) and v1.7.0 (0.3.3): nothing here blocks them — ledger uses none of the modules linen 1.6.x or 1.7.0 changed (1.6.2 only touches raw!; 1.7.0 adds modules moved from lode and lun). Each item names where it comes from; re-check before acting.

Moves into linen follow linen's AGENTS.md ("Importing external code"): the linen change and the deletion of ledger's copy happen in the same pass.

Correctness

• Close the reserve race. Ledger/Sql/Reserve.lean's insert … select … where (sum delta) − (sum held) ≥ amount is one statement, but under READ COMMITTED/REPEATABLE READ two concurrent reserves for the same org each read a snapshot without the other's uncommitted hold and can both insert — write skew, i.e. overspend. Nothing locks or constrains it; the module doc's "no advisory lock" is the gap, not a feature. Options: take pg_advisory_xact_lock(hashtextextended(org_id::text, 0)) inside the statement (e.g. as a CTE), lock the org's row (select … from orgs where id = $1 for update), or require callers to run it under SERIALIZABLE and retry on 40001. Any of these changes the contract liaison/Liaison/Budget.lean repeats — coordinate the change there (see "Reservation SQL is shared with liaison" below), update LedgerTests/Ledger/Sql/ReserveTest.lean, and add a live-Postgres concurrency test (none exists today). Until then the README flags it (the Guarantees table's "only under SERIALIZABLE" row and "Known gap" note, the Features bullet, the layout table), and the repository's double-spend-prevention topic states the intent, not a current guarantee. When it is closed, remove those flags and correct Reserve.lean's module doc, which still says the statement "actually prevents double-spend". (M)

• Consider putting the concurrency requirements in the types. Today no-overspend is enforced only by SQL text and by callers remembering the isolation level, while the rest of the guarantees are held by Lean types. Possible directions:

  • Index the transaction type by its isolation level, so that running reserve outside SERIALIZABLE does not type-check. Check first whether linen's Session/transaction API can carry this; if not, the change belongs in linen.
  • If the race is closed with a lock instead, make reserve take a token (e.g. OrgLock org) that can only be obtained by acquiring the per-org lock in the same transaction.
  • State no-overspend as a theorem over interleavings of reserve transactions against a model of Postgres, with the isolation level as an explicit hypothesis. This proves the design under stated assumptions, not the running database.

  Limits to keep in mind: types only constrain callers that go through Lean code. That can include liaison once it imports the reservation module (see "Reservation SQL is shared with liaison" below), but not writers that issue raw SQL, and it does not verify the SQL text itself. Depends on the choice made in "Close the reserve race" above. (M-L)

CI

• Build the executable, not only LedgerTests. CI runs lake build LedgerTests (.github/workflows/lean_action_ci.yml:16); no test imports Main, so the copied libpq link recipe is only exercised by the Docker publish. linen's AGENTS.md records a bug that only an executable link (Scrt1.o) exposes. Add lake build ledger, and a macOS leg for the lakefile's .dylib branch (lakefile.lean:49). (S)
• Verify the Docker image after the Actions bump. The publish workflow now uses docker/*-action v4/v6/v7 and actions/checkout@v7 (Node 24, deprecated inputs removed — none of which ledger uses), untested until the first push to main. The image could not be built locally (Docker Desktop and the registry need a corporate sign-in). Once it builds, consider moving the runtime from debian:bookworm-slim to trixie-slim (current stable; libpq.so.5 is the same soname), together with liaison, which uses the same base. (S)

Building blocks to share

• Typed environment readers. Main.lean:11-18 (DATABASE_URL → PoolSettings) is the same as liaison's Main.lean:14-26; lun and lode duplicate secondsEnv. ledger range-checks the port (Main.lean:30-36); lun, lode and liaison use toUInt16, which wraps. A System.Environment module in linen plus Settings.fromEnv, adopted by all four services. (S–M)
• A health check with a probe. linen's healthCheck (Linen/Network/WebApp/Extra/Middleware/HealthCheckEndpoint.lean:18-23) always answers 200, so Ledger/Health.lean:31-42 hand-rolls a 503 for a stopped sweeper; lun and liaison hand-roll theirs too. A healthCheckWith path probe in linen. (S)
• Reservation SQL is shared with liaison (liaison/Liaison/Budget.lean repeats Ledger/Sql/Reserve.lean). Application logic, so not linen: expose a pure module here that liaison imports. (M)

Workarounds that linen could remove

• libpq for consumers' executables. lakefile.lean:26-76 copies pkgConfig/pkgAbsoluteLibs (and a run_cmd defining the link flags) because Lake does not pass a dependency's moreLinkArgs to a dependent's executable; six repos carry the copy. An idea to try in linen: Lake 4.34 adds each imported library's moreLinkObjs to the executable link (Lake/Build/Module.lean:1297-1303), so a moreLinkObjs target yielding libpq's absolute path might carry it without the -L that shadows glibc. Unverified — prove it in linen's consumer CI job first. (M)
• One consumer native-dependency list. linen 1.7.0 ships it (ci/native-deps/apt.txt, and the setup-native-deps action with keyring: false); CI and the Dockerfile read it at the linen version lakefile.lean requires (0.3.3). (S)

Small

• Ledger/Sweeper.lean:56 sleeps with a UInt32 of milliseconds, which overflows past ~49 days of interval. (XS)