test(3vl): AND cod-override differentiator#78
Merged
Conversation
The cod override for the short-circuit connectives (checker.rs) special- cases OR *and* AND, but the vacuity-soundness suite only had a witness for OR (`x.status OR true`). Removing the `BinOp::And` arm from the override therefore broke no test, even though the AND override is load-bearing. Add the symmetric AND witness: `WHERE NOT (x.status AND false)`. `false` is AND's absorbing element, so at runtime `NOT (null AND false) = NOT false = true` keeps every row; under the strict (un-amended) cod, `x.status AND false : ⊥` then `NOT ⊥ : ⊥`, so the pattern is pruned as guaranteed_empty — the same static/dynamic unsoundness the OR override fixes. Verified as a real differentiator: deleting the AND arm from the override flips this query's guaranteed_empty to true and the test fails (the OR test is unaffected, so the two are independent witnesses). No semantics changed; test only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Felipe705x
force-pushed
the
test/3vl-and-cod-override-witness
branch
from
9257575 to
5da3cd5
Compare
Felipe705x
changed the title
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.
What
Follow-up to the merged 3VL work (#73, #76). Test only — no semantics changed.
The typechecker's
codoverride special-cases bothORandAND, but the suite only had a vacuity-soundness witness for OR (x.status OR true). Deleting theBinOp::Andarm from the override therefore broke no test — a real coverage gap, since the AND override is load-bearing.The AND witness
MATCH (x:N) WHERE NOT (x.status AND false) RETURN x.nameon a closed schema wherestatusis unknown (x.status : ⊥):falseis AND's absorbing element →null AND false → false→NOT false → true→ keeps all rows.x.status AND false : ⊥, thenNOT ⊥ : ⊥→ pattern pruned asguaranteed_empty.BoolsoNOT Bool : Booland the pattern is not pruned.The symmetry is the point: each short-circuit connective has an absorbing element yielding a defined value beside a
⊥/null operand —truefor OR (keeps rows directly),falsefor AND (keeps rows once negated).Verified as a real differentiator
Temporarily removing the
BinOp::Andarm from the checker'scodoverride flips this query'sguaranteed_emptytotrueand the new test fails; the existing OR test is unaffected. So the two are independent witnesses. Reverted; full suite 26/26, clippy clean.🤖 Generated with Claude Code