feat: built-in <DB> effect for SQL database access (Phase 1, #229) - #1144
Merged
Conversation
This was referenced Jul 23, 2026
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughAdds the built-in ChangesDB effect implementation
Validation and accounting
Estimated code review effort: 4 (Complex) | ~60 minutes Sequence Diagram(s)sequenceDiagram
participant VeraProgram
participant Compiler
participant WasmRuntime
participant SQLite
VeraProgram->>Compiler: compile effects(<DB>)
Compiler->>WasmRuntime: emit and register DB host imports
WasmRuntime->>SQLite: execute SQL with bound parameters
SQLite-->>WasmRuntime: rows, affected count, or error
WasmRuntime-->>VeraProgram: return Result value
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 6 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (6 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1144 +/- ##
==========================================
+ Coverage 93.77% 93.79% +0.02%
==========================================
Files 97 98 +1
Lines 33131 33315 +184
Branches 456 458 +2
==========================================
+ Hits 31067 31248 +181
- Misses 2051 2054 +3
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 8
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@CHANGELOG.md`:
- Around line 34-35: Update the DB effect entry in the changelog to state that
DB.execute and DB.query return an Ok/Err Result value that callers may propagate
directly or pattern-match, rather than claiming every call site must match it.
Preserve the existing Result error semantics and surrounding feature details.
In `@examples/README.md`:
- Line 52: Update the example count in examples/README.md to 41, changing the
existing “40 example programs” text while preserving the index entries and
surrounding documentation.
In `@spec/07-effects.md`:
- Line 400: Update the new fenced code block in the effects specification
documentation to include the language identifier vera, preserving the existing
example content and formatting.
In `@TESTING.md`:
- Around line 9-12: Update the corpus totals consistently: in TESTING.md lines
9-12, 645-647, and 748-750, replace outdated example counts with 41 and ensure
the test total is 8,420 where stated; in FAQ.md line 224, replace 7,992 tests
and 39 working example programs with 8,420 tests and 41 examples. No other
content changes are needed.
In `@tests/test_db_runtime.py`:
- Around line 83-95: Add a regression test alongside
test_execute_error_is_err_not_crash that calls _db_execute with
semicolon-separated CREATE TABLE and INSERT statements, then asserts the result
has the Err tag via _read_i32. Ensure the test verifies no sqlite3.Warning
escapes as a raised exception.
In `@tests/test_verifier_adt_decreases.py`:
- Around line 613-621: Update the current totals stated in the
test_overall_tier_counts docstring from 349/105/454 to 353/105/458 so they match
the existing assertions and documented tier counts.
In `@vera/runtime/db.py`:
- Around line 14-17: Revise the docstring near the sqlite3 parameter-binding
explanation so it does not claim injection is currently impossible. State that
parameter values are protected today, while the complete guarantee depends on
the future `#309` compile-time literal-SQL checker gate, and describe that as the
intended target state.
- Around line 79-108: The exception handlers in _db_query and _db_execute must
also catch sqlite3.Warning. Update both try/except blocks to handle
sqlite3.Warning alongside sqlite3.Error and return
_alloc_result_err_string(caller, str(exc)) so multi-statement SQL produces
Result.Err instead of escaping the host callback.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: b1d0e01d-96b7-4c96-a931-8a764d761a16
⛔ Files ignored due to path filters (7)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**examples/database.verais excluded by!**/*.veratests/conformance/ch09_db.verais excluded by!**/*.vera
📒 Files selected for processing (33)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdexamples/README.mdspec/07-effects.mdspec/09-standard-library.mdtests/conformance/manifest.jsontests/test_browser.pytests/test_db_effect.pytests/test_db_marshalling.pytests/test_db_runtime.pytests/test_verifier_adt_decreases.pytests/test_wasi_target.pyvera/_since.pyvera/browser/runtime.mjsvera/codegen/api.pyvera/codegen/assembly.pyvera/codegen/compilability.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/wasi.pyvera/environment.pyvera/runtime/db.pyvera/runtime/heap.pyvera/wasm/calls.pyvera/wasm/context.pyvera/wasm/inference.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Register the DB effect (query, execute) so effects(<DB>) and DB.query / DB.execute type-check. Phase 1 signatures are positional and stringly-typed: query(String, Array<Option<String>>) -> Result<Array<Array<Option<String>>>, String> execute(String, Array<Option<String>>) -> Result<Int, String> An Option<String> parameter / cell distinguishes a bound value (Some) from SQL NULL (None) — DESIGN principle 2, no implicit collapse to the empty string. Also stash the two SQL-executing OpInfo objects BY IDENTITY (db_sql_ops + is_db_sql_op) so the #309 literal-provenance gate keys on object identity, not the value-equal / user-shadowable op name. OpInfo is an unhashable, value-equal dataclass, so a name/set key would misfire on a user 'effect DB' look-alike. Mutation-validated: an ==/name key flips the look-alike test RED. Codegen/runtime wiring (marshalling, host binding, routing) and docs land in later stages of this branch. Skip-changelog: WIP feature stage; the DB effect CHANGELOG entry lands with the complete feature (#229 docs stage). Co-Authored-By: Claude <noreply@anthropic.invalid>
Add the heap marshalling for the DB effect boundary data, mirroring the existing
_alloc_* family with correct shadow-stack GC rooting:
- _read_wasm_array_of_options_of_string: inbound Array<Option<String>> params
reader (4-byte Option-ADT pointers; None tag 0, Some tag 1).
- _alloc_array_of_options_of_string / _alloc_result_ok_rows: outbound
Result.Ok(Array<Array<Option<String>>>) query grid (outer 8-byte
(row_ptr, n_cols) pairs; inner 4-byte Option pointers; 12-byte pair-payload
Result).
- _alloc_result_ok_i64: Result.Ok(Int) execute row-count (tag + i64, 16 bytes).
Tested via an InstanceCaller over a real compiled GC module (pure programs
instantiate with no host imports), each case run normally AND under
VERA_EAGER_GC=1 so every $alloc fires $gc_collect. Mutation-validated:
dropping the outer-backing root SIGBUSes the swept-pointer read under eager GC;
dropping the cell-backing root fails the large-grid round-trip — both roots
load-bearing.
register_db wiring + the DB ops that consume these land in the next stage.
Skip-changelog: WIP feature stage; the DB effect CHANGELOG entry lands with the complete feature (#229 docs stage).
Co-Authored-By: Claude <noreply@anthropic.invalid>
vera/runtime/db.py — the <DB> effect host functions, mirroring register_inference:
- _open_connection: VERA_DB_URL config (:memory: spellings + sqlite:///path;
hermetic in-memory default), one connection per program run so state built
by one call is visible to the next.
- _db_query / _db_execute: run a statement via sqlite3 and marshal
Result.Ok(rows) / Result.Ok(rowcount) or Result.Err(message) — a DB error is
an Err value, never a crash — through the S2 helpers.
- register_db(linker, ops_used, env_vars): bind db_query / db_execute closures
that read (sql, params) from WASM memory and call the impls.
Parameters bind through ? placeholders (sqlite3 parameterisation), so a value is
never interpreted as SQL; with the #309 literal-SQL gate, injection is impossible
by construction (test: a "'; DROP TABLE" param binds as a literal, the table is
intact). Phase 1 is stringly-typed: cells are str / None (NULL).
Codegen routing (call $vera.db_query), the api.py register_db call, and the
db_ops_used CompileResult threading land in S4 (end-to-end).
Skip-changelog: WIP feature stage; the DB effect CHANGELOG entry lands with the complete feature (#229 docs stage).
Co-Authored-By: Claude <noreply@anthropic.invalid>
Wire DB.query / DB.execute through codegen so a Vera program using <DB> compiles
and runs end-to-end against sqlite:
- calls.py: "DB" joins the host-import qualifiers; DB.<op> emits
`call $vera.db_<op>` and records _db_ops_used.
- db_ops_used is threaded like inference_ops_used — inited on both WasmContext
and CodeGenerator, merged per-function, carried through all four
CompileResult constructions (the #808 fan-in), and register_db(...) is
called in api.py execute().
- context.py / inference.py: both DB ops are non-void, returning an i32 Result
ADT pointer.
- assembly.py: db_query / db_execute WAT import sigs (param i32x4 result i32).
- compilability.py: DB joins the E603 effect whitelist + the op pre-scan.
End-to-end tests: a CREATE + parameterised INSERT (incl. a NULL param) + SELECT
round-trips to a 2-row grid; a DELETE returns its rowcount; the query survives
VERA_EAGER_GC=1 (S2 rooting through the real host path); and an injection-looking
param binds as a literal, leaving the table intact. 173 existing host-effect
tests unaffected.
Skip-changelog: WIP feature stage; the DB effect CHANGELOG entry lands with the complete feature (#229 docs stage).
Co-Authored-By: Claude <noreply@anthropic.invalid>
- wasi.py: <DB> joins _UNSUPPORTED_FAMILIES — a program compiled with
--target wasi-p2 is rejected with the family diagnostic (naming `db`),
never a silent fallback (there is no sqlite host under wasi-p2).
- browser/runtime.mjs: db_query / db_execute are deliberate Result.Err stubs
(a database driver + credentials can't live safely in client-side JS),
mirroring the Inference stub; both ops' Err arm is Result<_, String>, so the
12-byte Err layout (allocResultErrString) serves either. A DB program links
and runs in the browser, taking the Err arm — never a LinkError.
Tests: the wasi family gate rejects a DB program (rc=1; diagnostic names db, no
artifact written); the browser stub makes DB.query / DB.execute take the Err arm
under the Node harness.
Skip-changelog: WIP feature stage; the DB effect CHANGELOG entry lands with the complete feature (#229 docs stage).
Co-Authored-By: Claude <noreply@anthropic.invalid>
…L, CHANGELOG (S6) Completes the <DB> effect Phase 1. Adds an offline examples/database.vera (sqlite::memory:, create + parameterised insert with a NULL cell + query + row-count assertion) and a run-level ch09_db conformance program; spec §7.7.7 (the DB effect) and §9.5.7 (row/parameter marshalling); the SKILL.md DB section and two Known-Limitations rows (#372 handlers, #1143 Phase 2/3 scope); the accumulated CHANGELOG [Unreleased] entry; and the doc-count reconcile (164 conformance, 41 examples, 8420 tests, 211 corpus) plus regenerated site assets. Files the Phase 2/3 tracking issue (#1143). No version bump: rides [Unreleased] until the v0.1.7 cut. Co-Authored-By: Claude <noreply@anthropic.invalid>
pr-review-toolkit findings on the #229 DB effect PR: - **Comment overclaim (honesty).** Comments in db.py / environment.py described the #309 literal-provenance gate as already enforcing ("injection is impossible by construction"; "rejects a non-literal, so injection is a compile error") — but #309 is a separate, later PR. Corrected to state the runtime `?`-parameterisation guarantee (in force now) and the compile-time literal-SQL gate as forthcoming, matching the spec, which was already accurate. - **Connection-open errors escaped as a traceback.** register_db opened the sqlite3 connection eagerly and unguarded, so an unopenable VERA_DB_URL raised sqlite3.OperationalError during setup — an uncaught host crash that bypassed the program's own `match { Err(...) }`, the one DB error that was not a value. The open is now deferred: on failure each op returns the captured error as Err when invoked, the same contract as a driver error. - **Browser-stub layout comment.** Corrected "12-byte layout shared by both Ok payload shapes" — a Result is tag-dispatched, and Ok(Int) is 16 bytes, not 12; a fully-formed Err is valid regardless of the Ok variant's size. - **Coverage.** Added the CREATE-TABLE rowcount -1 sentinel, a BLOB cell UTF-8-decoded with replacement, and the bad-URL -> Err end-to-end path. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
feat/229-db-effect
branch
from
July 23, 2026 13:55
e8b0310 to
4ddcbbc
Compare
Owner
Author
pr-review-toolkit review + fixes appliedRan the review toolkit (code-reviewer, silent-failure-hunter, pr-test-analyzer, comment-analyzer) over the Fixed in this round:
Verified clean — no action needed:
Also: rebased onto |
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (2)
examples/README.md (1)
52-52: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the example count.
Adding
database.verabrings the index to 41 example programs, but the heading still says 40. Update the heading so it matches the index.Proposed fix
-40 example programs demonstrating Vera's features. +41 example programs demonstrating Vera's features.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/README.md` at line 52, Update the examples index heading in README.md from 40 to 41 to match the addition of database.vera; leave the example entries unchanged.Sources: Path instructions, Learnings
spec/07-effects.md (1)
400-400: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winMark the DB example as Vera.
Line 400 lacks a language identifier, triggering MD040 and preventing documentation tooling from recognising the block as Vera.
Proposed fix
-``` +```vera🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@spec/07-effects.md` at line 400, Update the fenced code block at the referenced DB example in spec/07-effects.md by adding the vera language identifier to its opening fence, so documentation tooling recognizes the block as Vera and MD040 is satisfied.Sources: Path instructions, Linters/SAST tools
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@vera/runtime/heap.py`:
- Around line 1119-1139: Update _read_wasm_array_of_options_of_string to
validate the guest-controlled pointer array range before iterating, ensuring ptr
plus count times four stays within WASM memory and raises the established
out_of_bounds trap instead of allowing an invalid _read_i32 access. Preserve the
existing decoding behavior for valid arrays; leave the nested opt_ptr field
reads out of scope.
---
Duplicate comments:
In `@examples/README.md`:
- Line 52: Update the examples index heading in README.md from 40 to 41 to match
the addition of database.vera; leave the example entries unchanged.
In `@spec/07-effects.md`:
- Line 400: Update the fenced code block at the referenced DB example in
spec/07-effects.md by adding the vera language identifier to its opening fence,
so documentation tooling recognizes the block as Vera and MD040 is satisfied.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 525919d4-63a6-43e4-9e20-5b19bca54fdd
⛔ Files ignored due to path filters (7)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**examples/database.verais excluded by!**/*.veratests/conformance/ch09_db.verais excluded by!**/*.vera
📒 Files selected for processing (33)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdexamples/README.mdspec/07-effects.mdspec/09-standard-library.mdtests/conformance/manifest.jsontests/test_browser.pytests/test_db_effect.pytests/test_db_marshalling.pytests/test_db_runtime.pytests/test_verifier_adt_decreases.pytests/test_wasi_target.pyvera/_since.pyvera/browser/runtime.mjsvera/codegen/api.pyvera/codegen/assembly.pyvera/codegen/compilability.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/wasi.pyvera/environment.pyvera/runtime/db.pyvera/runtime/heap.pyvera/wasm/calls.pyvera/wasm/context.pyvera/wasm/inference.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…sion (#1144) CodeRabbit findings on #1144 (rounds 1 & 2): - db.py: catch sqlite3.Warning alongside sqlite3.Error in the query / execute / connection-open handlers. Warning is a DB-API *sibling* of Error (not a subclass), so multi-statement SQL — which raises Warning on some Python versions, ProgrammingError on others — surfaces as Result.Err instead of escaping the host callback. Regression test added. - heap.py: bounds-check _read_wasm_array_of_options_of_string's guest-controlled pointer array (ptr + count*4 within WASM memory) before the walk, raising a clean out_of_bounds trap instead of SIGBUS in _read_i32 — the #1145 class one level up from the string payload read (which #1145 already guards). Regression test added; the nested opt_ptr field reads are scoped out as a follow-up. - test_verifier_adt_decreases: correct the test_overall_tier_counts docstring summary (349/105/454 -> 353/105/458) to match the assertions. - CHANGELOG: the DB Result is propagated or matched by callers, not "must match". - Doc counts: examples/README, TESTING and FAQ prose to 41 examples; FAQ total. Also: the status string listed "nine algebraic effects (..., Random, Diverge)" and omitted the new DB effect — corrected to "ten ... Inference, DB, Random, Diverge" in README.md, docs/index.html, and scripts/build_site.py (docs/ regenerated). Skipped (with reason): the spec §7.7.7 `effect DB {}` fence stays bare ``` — parity with the sibling Random / IO / Async effect-declaration fragments; MD040 is not enforced in this repo, and tagging only it `vera` would trip the parse gate (an `effect {}` fragment is not a standalone parseable program). The db.py injection-docstring finding was already fixed in the earlier review round. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@FAQ.md`:
- Around line 224-225: Update the aggregate test count in FAQ.md from 8,429 to
8,431, keeping the existing conformance-suite and example-program counts
unchanged.
In `@vera/runtime/heap.py`:
- Around line 1139-1148: Update the DB parameter handling around the outer
ptr/count guard to reject negative count values and validate each guest-supplied
Option pointer before dereferencing it. Before reading each tag with _read_i32,
ensure four bytes are in bounds; for Some(String) entries, validate the complete
12-byte layout before reading payload fields, raising WasmtimeError on invalid
ranges while preserving valid None/Some processing.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: a75dfec5-584d-4eb0-8cc7-be45bcc0f42a
⛔ Files ignored due to path filters (4)
docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**
📒 Files selected for processing (12)
CHANGELOG.mdFAQ.mdREADME.mdROADMAP.mdTESTING.mdexamples/README.mdscripts/build_site.pytests/test_db_marshalling.pytests/test_db_runtime.pytests/test_verifier_adt_decreases.pyvera/runtime/db.pyvera/runtime/heap.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
) On-disk `<DB>` example (requested): - `examples/sqlitedb.vera` reads a committed `examples/sqlitedb.sqlite` fixture (cities table; 'Atlantis' has a NULL country). It prints one line per city — rendering each nullable cell through `option_unwrap_or(_, "NULL")` so the SQL NULL is visible and distinct from "" — and returns the row count. Graceful either way: without `VERA_DB_URL` it falls back to `:memory:`, takes the Err arm, and prints how to point at the file (both arms exit 0). - `tests/test_db_runtime.py`: a golden-output test runs the actual example file against the committed fixture with `VERA_DB_URL` set and pins the rendered table + the NULL rendering. CI's `check_examples` only checks/verifies examples and this one exits 0 either way, so without this test the on-disk read path — the whole point of the example — never executes in CI. It also smoke-tests that the committed `.sqlite` is intact. CodeRabbit round 3 (three open findings): - heap.py:1148 — `_read_wasm_array_of_options_of_string` now bounds-checks every guest-controlled offset before it reaches the unchecked `_read_i32`: reject a negative count, validate each element `opt_ptr` before its tag read, and validate the full 12-byte `Some(String)` cell before its field reads. The outer-array guard alone left the per-element pointers able to SIGBUS — the #1145 class one level deeper. Three regression tests (negative count, element pointer OOB, Some cell straddling the memory end). - build_site.py:86 — the generated `llms.txt` effect enumerations were incomplete: the intro listed nine effects (missing Diverge) and the Chapter 7 line omitted DB. Both now list all ten; assets regenerated. - FAQ.md test count 8,429 -> 8,444. ROADMAP: `#229 database effect` deleted from the horizon (this PR closes it); `#309 contract-verified SQL` kept (no longer blocked behind #229) and `#1143` (`<DB>` phases 2-3: named columns, typed rows) added as the DB continuation. Doc-count reconciliation for the new example + tests: 41 -> 42 examples, 8,431 -> 8,444 tests, 211 -> 212 corpus, per-file test/line rows, and the `test_overall_tier_counts` totals (353/105/458 -> 357/105/462; sqlitedb adds 4 Tier-1 obligations). Site assets regenerated. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@examples/README.md`:
- Line 53: Update the sqlitedb.vera command in the examples table to set
VERA_DB_URL=sqlite:///examples/sqlitedb.sqlite before invoking vera run, so it
reads the committed on-disk SQLite fixture described in the row instead of the
default in-memory database.
In `@FAQ.md`:
- Around line 224-225: Update the working example-program count in FAQ.md from
41 to 42, leaving the conformance-suite count and surrounding documentation
unchanged.
In `@tests/test_db_runtime.py`:
- Around line 268-299: The test method
test_reads_committed_fixture_and_prints_city_table should stop using
monkeypatch.setenv to configure VERA_DB_URL. Pass the URL explicitly through
execute using its env_vars argument, preserving the existing portable sqlite URL
and all assertions.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: e0b3005e-9bac-4677-ac25-372616a02dba
⛔ Files ignored due to path filters (5)
docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**examples/sqlitedb.verais excluded by!**/*.vera
📒 Files selected for processing (15)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdREADME.mdROADMAP.mdTESTING.mdexamples/README.mdexamples/sqlitedb.sqlitescripts/build_site.pytests/test_browser.pytests/test_db_marshalling.pytests/test_db_runtime.pytests/test_verifier_adt_decreases.pyvera/runtime/heap.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…reading (#1144) - FAQ.md: "41 working example programs" -> 42. The count reconcile grepped for "41 example" and missed the "41 working example" wording variant. - examples/README.md: the sqlitedb Run command now sets VERA_DB_URL so it actually reads the committed fixture the row advertises (the bare command fell back to the in-memory default). The golden-output test covers execution. - tests/test_db_runtime.py: the on-disk-example test threads the DB URL through execute(env_vars={...}) rather than mutating os.environ via monkeypatch, matching the explicit-dict form the _open_connection unit tests use. - TESTING.md: test_db_runtime.py line count 299 -> 301. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
TESTING.md (1)
9-12: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winClarify the 40-example Tier 1 count. TESTING.md:17 still says “across the 40 examples verified statically (Tier 1)”, while the overview and the rest of the file refer to all 42 examples. If 40 is a deliberate subset, say so explicitly; otherwise update it to 42.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@TESTING.md` around lines 9 - 12, Resolve the example-count inconsistency in TESTING.md by updating the Tier 1 wording to 42 if it refers to all examples, or explicitly identify the deliberate 40-example subset if that distinction is intended. Keep the overview and other example counts consistent with the chosen interpretation.Sources: Path instructions, Learnings
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@TESTING.md`:
- Around line 9-12: Resolve the example-count inconsistency in TESTING.md by
updating the Tier 1 wording to 42 if it refers to all examples, or explicitly
identify the deliberate 40-example subset if that distinction is intended. Keep
the overview and other example counts consistent with the chosen interpretation.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: aaced4b8-a1d4-4394-8f49-5c0d6fbd8365
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (4)
FAQ.mdTESTING.mdexamples/README.mdtests/test_db_runtime.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…o 42 / 357-462 (#1144) CodeRabbit outside-diff finding: TESTING.md's overview said 42 examples while the Tier-1 "Contract verification" row and the "live sums" section still read 40 examples / 349-of-454 obligations — stale since before both database.vera and sqlitedb.vera (each +4 Tier-1). Updated to the current authoritative totals that test_overall_tier_counts asserts (357 Tier-1 / 105 Tier-3 / 462 total, 77.3% static) and 42 examples at every site: the overview Tier-1 row, the live-sums table, the check_examples.py command comment, and the feature-coverage rows. No deliberate 40-example subset exists; all refer to the full corpus.
Owner
Author
|
@coderabbitai Fixed — the "40 examples" was stale across TESTING.md, not a deliberate subset: the Tier-1 "Contract verification" overview row, the "live sums" table, the |
|
Tip For best results, initiate chat on the files or code changes.
|
This was referenced Jul 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a built-in
<DB>effect for executing SQL against a relational database (Phase 1 of #229).DB.executeruns writes (CREATE/INSERT/UPDATE/DELETE) and returns the affected-row count;DB.queryruns aSELECTand returns the result grid. Both returnResult<_, String>, so a driver error is a value the caller mustmatch, never a trap.This is the effect and its runtime. The compile-time literal-SQL guarantee — SQL injection as a type error — is the next PR, #309, which builds on the
db_sql_opsidentity stash added here. At runtime, parameter binding already keeps data out of SQL syntax.Design decisions
Array<Array<Option<String>>>, parametersArray<Option<String>>. A cell isSome(text), orNonefor SQLNULL, soNULLand""stay distinct (DESIGN principle 2, no implicit behaviour). ANOT NULLcolumn is read withoption_unwrap_or(cell, "").?placeholders —Some(v)a value,NoneaNULL— so data never becomes SQL syntax.VERA_DB_URL(sqlite::memory:default, orsqlite:///path).handle[DB]awaits Inference effect: user-defined handlers (handle[Inference]) #372.Errfor every DB op (deliberate stub);vera compile --target wasi-p2rejects<DB>at compile time.What's included
db_sql_opsidentity stash (environment.py,_since.py) — keyed byOpInfoidentity so a usereffect DB { ... }never trips the built-in machineryruntime/heap.py), mutation-validated and differential-tested underVERA_EAGER_GC=1sqlite3(runtime/db.py,register_db)db_ops_usedthreaded through the compile pipeline (the Preciseoverflowtrap kind for #798 integer-overflow traps (currentlyunreachable) #808 fan-in pattern)Errstubexamples/database.vera(offline,sqlite::memory:) and a run-levelch09_dbconformance programTesting
test_db_effect.py(checker),test_db_marshalling.py(GC round-trips + eager-GC variants),test_db_runtime.py(end-to-end SQLite), plus browser-stub and wasi-gate testsexamples/database.verapassescheck+verify+run(exit 0, exactly 2 rows), including underVERA_EAGER_GC=1Follow-ups
Inference.embed) stays open — this PR added the DB-specific marshalling only, not the genericArray<Float64>host-return path. (Deliberately not linked as a closing reference.)Closes #229.
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
<DB>effect for SQLite database access viaDB.queryandDB.execute, with positional parameter binding,NULL→Nonemapping, affected-row counts, andResult-based error handling.Documentation
<DB>usage andVERA_DB_URLconfiguration, along with current limitations and updated conformance/example corpus counts.Tests
<DB>coverage for typing, ABI marshalling, runtime behaviour, browser stubs, andwasi-p2rejection.