Repository navigation
fix(postgres): give a host's row-count catalog its views' keys - #126
Merged
Merged
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Contributor
There was a problem hiding this comment.
ℹ️ No critical issues. One edge case where the catalog settles early, inline.
Reviewed changes
I reviewed the change that makes postgres::catalog() follow views the same way the analysis does.
catalog()reads views: it prefetches the relations' columns, follows each view (a view over a view too) withEngine::viewed, askscatalog_rowsfor the tables those views read, merges their keys withmerge_keysand setscatalog.views. This matches the analysis path atpostgres.rs:696-742.- Unit test:
the_row_count_catalog_reads_a_view_by_the_keys_its_statement_keepschecks a read by key through a view of a view (at most one row) and a read by another column (not bounded). I ran it locally and it passes. engine.wasm: rebuilt for the new Postgres fingerprint.
claude-opus-5-5 ｜ 𝕏
A host that runs the row-count proof itself asks catalog() for the relations a statement reads. Views among them came with no defining statement and none of the keys of the tables they read, so a read by key through a view was never pinned, as an analysis pins it since #105.
viewed dropped each prefetch it issued, and which list a relation was asked in turned on how many views were known yet, so a round could settle with a view over a view still unread: a read by key through it went unpinned. It now answers only once every prefetch is answered.
colinhacks
force-pushed
the
catalog-view-keys
branch
from
October 26, 2026 19:27
d16dc4f to
6aec1ca
Compare
Contributor
There was a problem hiding this comment.
✅ No new issues found. The early-settle case is fixed.
Reviewed changes
I reviewed 6aec1ca, which makes Engine::viewed wait until every prefetch it issued has an answer.
viewedreturnsLazy<…>: it now returnsNonewhile anyprefetch(&unread)is still unanswered, instead of dropping that result. The replay still converges, because the set of known views only grows each round. Once every view is known, the traversal and its prefetch lists stay the same from round to round.- Both callers wait on it:
catalog()uses?, andrun()addsviewedto itslet … else { return None }guard. As a result, the analysis no longer settles with a nested view still unread. - Regression test: the catalog test now settles the
a_v/c_v → x → y → todoslayout to all four views, and checks that a read by key throughc_vreturns at most one row. engine.wasm: rebuilt.
claude-opus-5-5 ｜ 𝕏
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
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.
A Rust host that runs the row-count proof itself asks
postgres::catalog()for the catalog of the relations a statement reads. Since #105 an analysis pins a read by key through a view, reading the view's defining statement and the keys of the tables it reads, butcatalog()gathered neither, so such a host never pinned one.catalog()now reads the relations' columns as an analysis does, follows each view among them (a view over a view too) with the analysis's ownviewed, and merges the keys of the tables they read.vieweddropped each prefetch it issued, and which list a relation was asked in turned on how many views were known yet, so a round could settle with a view over a view still unread. It now answers only once every prefetch is answered, forcatalog()and the analysis alike.catalog()over a view of a view, and over two views whose chains meet, and proves a read by key through them is at most one row, and a read by another column is not.packages/postgres/engine.wasmis rebuilt; the Postgres oracle cases pass unchanged.