sre/track2i: Phase 4 — relation-aware join in distributive/SD checks#59
Open
kumavis wants to merge 4 commits into
Open
sre/track2i: Phase 4 — relation-aware join in distributive/SD checks#59kumavis wants to merge 4 commits into
kumavis wants to merge 4 commits into
Conversation
Fixes test-sre-sd-properties.rkt CI failures. Phase 3 (commit bd1179b) shipped the sweep + tests in an "in-progress" state because test-distributive, test-sd-vee/detailed, and test-sd-wedge/detailed in sre-core.rkt hardcoded `'equality` for the join lookup. When the sweep asked for type×subtype distributive, it paired the subtype-aware meet with the equality join — mixing lattices and refuting distributivity for purely structural reasons rather than for any algebraic content of the type lattice. Phase 4 thread the relation through: - test-distributive, test-sd-vee/detailed, test-sd-wedge/detailed, test-sd-vee, test-sd-wedge gain a `#:relation [relation 'equality]` keyword. The join is looked up via `((sre-domain-merge-registry domain) relation)`, matching the meet's relation. Default 'equality preserves the behavior of every existing positional caller (test-sre-algebraic.rkt unchanged). - sre-property-sweep.rkt's run-sd-sweep passes #:relation rel so the sweep stays inside one lattice per (domain, relation) check. - infer-domain-properties already took #:relation; it now passes that through to the underlying tests so any future non-equality inference path is correct-by-construction. Per Track 2H's declared subtype properties (unify.rkt:115: distributive prop-confirmed, has-pseudo-complement prop-confirmed) and the Phase 3c hand-picked-6 confirmation for type×equality, both test-sre-sd-properties.rkt load-bearing assertions (equality-distributive, subtype-distributive) should now confirm at depth-0 (216 triples × 6 checks). Refs: docs/tracking/2026-04-30_SRE_TRACK2I_SD_CHECKS_DESIGN.md § Phase 4.
Phase 3 sweep test "each finding has correct shape" used `(check-true (memq value list))`, but `memq` returns the matched sublist (e.g., `(equality subtype)` or `(subtype)`), not `#t`. `check-true` requires exactly `#t`, so the membership assertions failed even when the values were members of the expected sets. Switched to `check-not-false`, which is the rackunit idiom for "value is truthy". Caught locally after building Racket v9.0 from source and running the test: before: 1/8 test failures (this case) after: 8 tests passed test-sre-algebraic.rkt (63 tests) and test-sre-track2h.rkt (35 tests) remain green.
There was a problem hiding this comment.
Pull request overview
This PR fixes Track 2I semidistributivity/distributivity checks by making the join used in test-distributive / SD checks relation-aware, so subtype-based checks don’t accidentally combine a subtype meet with an equality join (mixing lattices and producing structurally spurious refutations). This aligns the sweep with the intended “one lattice per (domain, relation)” behavior and addresses the CI failures in test-sre-sd-properties.rkt.
Changes:
- Thread
#:relation(defaulting to'equality) throughtest-distributive,test-sd-vee(/detailed), andtest-sd-wedge(/detailed)so join lookup matches the meet relation. - Update
run-sd-sweepto pass#:relation relto the distributive + SD checks. - Fix the test assertions in
test-sre-sd-properties.rktto correctly assert membership checks (memqreturns non-#f, not necessarily#t).
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| racket/prologos/tests/test-sre-sd-properties.rkt | Fixes membership assertions so Phase 3 findings validation doesn’t incorrectly expect memq to return #t. |
| racket/prologos/sre-property-sweep.rkt | Ensures the sweep passes the relation through to distributive + SD checks, keeping each check within one lattice. |
| racket/prologos/sre-core.rkt | Adds #:relation to distributive/SD test helpers and threads it through infer-domain-properties for those meet-dependent properties. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
512
to
+516
| (define props-3 | ||
| (if meet-fn | ||
| (update-property props-2 'distributive | ||
| (test-distributive domain samples meet-fn)) | ||
| (test-distributive domain samples meet-fn | ||
| #:relation relation-name)) |
Contributor
Author
There was a problem hiding this comment.
Good catch — fixed in ea0e4fb. test-commutative-join / test-associative-join / test-idempotent-join now take #:relation [relation 'equality] and use ((sre-domain-merge-registry domain) relation) for the join lookup; infer-domain-properties threads relation-name through. Default 'equality keeps every existing positional caller (test-sre-algebraic.rkt, test-facet-sre-registration.rkt) unchanged. Verified locally on Racket v9.0: 8 + 63 + 35 + 21 = 127 tests still green across the four affected files.
Generated by Claude Code
Copilot review on PR #59 noted that test-commutative-join, test-associative-join, and test-idempotent-join still hardcoded the 'equality join lookup. infer-domain-properties is parametrised on #:relation, so calling it for any non-equality relation would have computed the join axioms in the equality lattice but stored the results under the non-equality relation's property hash — exactly the lattice-mixing pattern the previous commit fixed for distributive / SD. Add #:relation [relation 'equality] to the three join-axiom tests and have infer-domain-properties pass relation-name through. Default 'equality preserves every existing positional caller (test-sre-algebraic.rkt, test-facet-sre-registration.rkt). Verified locally with Racket v9.0: test-sre-sd-properties.rkt : 8 tests passed test-sre-algebraic.rkt : 63 tests passed test-sre-track2h.rkt : 35 tests passed test-facet-sre-registration.rkt : 21 tests passed
Two-pronged coverage expansion for the keyword Phase 4 added:
(a) test-sre-algebraic.rkt: three unit tests calling
test-commutative-join / test-associative-join / test-idempotent-join
with #:relation 'subtype on the type domain. Documents the keyword
contract; cannot distinguish between equality and subtype merges
because commutativity/associativity/idempotence happen to hold under
both for these samples (called out in the comment).
(b) test-sre-sd-properties.rkt: one integration test calling
infer-domain-properties with #:relation 'subtype + the
subtype-aware meet. Verifies all six axioms (commutative /
associative / idempotent / distributive / sd-vee / sd-wedge) resolve
to prop-confirmed for the type domain. This is the load-bearing
regression guard — manually verified by sabotaging
test-distributive to hardcode 'equality and confirming the test
refutes (and restoring confirms 9/9 again).
Verified locally on Racket v9.0:
test-sre-sd-properties.rkt : 8 → 9 tests passed
test-sre-algebraic.rkt : 63 → 66 tests passed
test-sre-track2h.rkt : 35 tests passed (unchanged)
test-facet-sre-registration.rkt : 21 tests passed (unchanged)
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.
Fixes test-sre-sd-properties.rkt CI failures. Phase 3 (commit bd1179b)
shipped the sweep + tests in an "in-progress" state because
test-distributive, test-sd-vee/detailed, and test-sd-wedge/detailed in
sre-core.rkt hardcoded
'equalityfor the join lookup. When the sweepasked for type×subtype distributive, it paired the subtype-aware meet
with the equality join — mixing lattices and refuting distributivity for
purely structural reasons rather than for any algebraic content of the
type lattice.
Phase 4 thread the relation through:
test-distributive, test-sd-vee/detailed, test-sd-wedge/detailed,
test-sd-vee, test-sd-wedge gain a
#:relation [relation 'equality]keyword. The join is looked up via
((sre-domain-merge-registry domain) relation), matching the meet'srelation. Default 'equality preserves the behavior of every existing
positional caller (test-sre-algebraic.rkt unchanged).
sre-property-sweep.rkt's run-sd-sweep passes #:relation rel so the
sweep stays inside one lattice per (domain, relation) check.
infer-domain-properties already took #:relation; it now passes that
through to the underlying tests so any future non-equality inference
path is correct-by-construction.
Per Track 2H's declared subtype properties (unify.rkt:115:
distributive prop-confirmed, has-pseudo-complement prop-confirmed) and
the Phase 3c hand-picked-6 confirmation for type×equality, both
test-sre-sd-properties.rkt load-bearing assertions
(equality-distributive, subtype-distributive) should now confirm at
depth-0 (216 triples × 6 checks).
Refs: docs/tracking/2026-04-30_SRE_TRACK2I_SD_CHECKS_DESIGN.md § Phase 4.