Repository navigation
feat(postgres): read bounds, a divisor and a pattern from a check - #200
colinhacks wants to merge 2 commits into
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub. 1 Skipped Deployment
|
There was a problem hiding this comment.
Important
Two ways the new CHECK reading can produce a descriptor that is wrong: a cast that rounds its constant gives an unsound bound, and an integer CHECK no value can meet gives a minimum above its maximum. Both are inline.
Reviewed changes
I reviewed the whole PR: the Postgres engine reading bounds, a divisor and a pattern from a CHECK, how those reach columns, whole rows and written parameters, and the oracle checks that come with it.
check_facts— parses theCHECKtext the server prints. It reads eachANDconjunct and the one test besidecolumn IS NULL, and only uses built-in operators, resolved throughTrust.CheckFacts— combines bounds by taking the tighter one, and leaves out a bound the type's width ornumeric(p,s)already implies.- Plumbing — the facts follow the same paths
non_finitealready uses: bare result columns, JSON shapes, stored whole-row fields, and bare written parameters.CHECKS_QUERYnow coversint2,int4andint8. - Oracle —
fact_contradictionholds seeded values to their bounds, divisor andlike/ilikepattern. The newcheck_factscase is added, and four otherexpected.txtfiles gain facts.
claude-opus-5-5 ｜ 𝕏
A cast can round its constant, and a real compares with a double precision widened, so a stored value can pass past the constant the check prints. An integer check no value meets now gives no bounds once its exclusive bounds are made inclusive.
There was a problem hiding this comment.
✅ No new issues found. Both earlier findings are fixed, and each has a test.
Reviewed changes
I reviewed the one commit since the last review, 12c54ee. It stops reading a bound when a cast or a float's width changes the constant the CHECK prints, and it leaves out integer bounds that no value can meet.
- Rounding casts:
number()reads through a cast only when the cast keeps its value. To an integer type, the constant has to be whole. Torealordouble precision, it has to print back as itself. Fromrealtodouble precision,realhas to hold it exactly. A cast from a float tonumeric, or to a type with a modifier (numeric(3,1)), gives no bound. - Widened comparisons: a
realcolumn checked against adouble precisionconstant, or the reverse, gives a bound only whenrealholds the constant exactly. Soreal 0.1passing> 0.1gives no bound. - Unmeetable bounds:
CheckFacts::applyleaves the bounds out when they are equal and either one is exclusive. The integer arm now checks after turning exclusive bounds into inclusive ones, against the type's own range, sox > 5 and x < 6andx > 2147483647onint4give no bounds. - Tests: new engine assertions cover each form. The new
roundingstatement inoracle/cases/check_factsseeds the values that broke the old bounds (2.9under<= 2.5::int,real 0.1under> 0.1).
claude-opus-5-5 ｜ 𝕏
The Postgres engine now reads three more facts from a
CHECKinto a column's type: a number's bounds, its divisor and a string's pattern. These fields were in the format, but no engine wrote them.age int check (age between 0 and 150){ "kind": "integer", "bits": 32, "min": "0", "max": "150", "name": "int4" }pos int check (pos > 0){ "kind": "integer", "bits": 32, "min": "1", "name": "int4" }rate numeric check (rate > 0 and rate < 1)"exclusive_min": "0", "exclusive_max": "1"qty int check (qty % 5 = 0)"multiple_of": "5"slug varchar(20) check (slug like 'a%')"pattern": { "dialect": "like", "source": "a%" }code text check (code ~ '^[a-z]+$')"pattern": { "dialect": "postgres", "source": "^[a-z]+$" }note text check (note ~* 'abc')"pattern": { "dialect": "postgres", "source": "(?i)abc" }A domain's
CHECKcounts the same way, and so does a field read through a table's whole row. A bare parameter written to such a column takes these facts too. TypeScript types and.run()don't change.What it reads
AND, and the one test besidecolumn is nullunder anOR.int2,int4,int8, floats andnumeric.column % n = 0. A divisor of 1 says nothing and is left out.like,ilike,~and~*with a constant, ontextorvarcharunder a deterministic collation.CHECKrules resolve them.What it leaves out
not, or any otheror, which may not bind every row.smallint check (x >= -40000)or one past anumeric(p,s)'s reach.CHECKno value can meet (x > 5 and x < 1).char(n)'s pattern, since its padding is read back.Tests
oracle/cases/check_factsis new: 11 statements, all of which run. The oracle now holds every value to its bounds, divisor andlikeorilikepattern. A regular expression is left to the server, which already refused any row it doesn't match.expected.txtchange, 10 lines, each only gaining a fact from aCHECKthe case declares.CHECKgives.CHECKS_QUERYnow reads integer columns.tests/catalog-queries.test.tsholds it to the same answers under a hostile search path.Verified
cargo build --workspace --all-targetswith no warning; the Postgres engine's tests (204) and core's.--strict-coverage: none failed.nub run typecheck, andnub run testagainst Postgres 18 and MySQL 8.4 on the release binary: 365 passed, none skipped.nub run captureinsite/writes the same files.