From e30b2ddd36377e8dbb7b8fc8c933680195cb0191 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 6 May 2026 01:46:57 +0000 Subject: [PATCH 1/4] =?UTF-8?q?sre/track2i:=20Phase=204=20=E2=80=94=20rela?= =?UTF-8?q?tion-aware=20join=20in=20distributive/SD=20checks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- racket/prologos/sre-core.rkt | 40 +++++++++++++++++--------- racket/prologos/sre-property-sweep.rkt | 6 ++-- 2 files changed, 30 insertions(+), 16 deletions(-) diff --git a/racket/prologos/sre-core.rkt b/racket/prologos/sre-core.rkt index 78fbdae75..79937853a 100644 --- a/racket/prologos/sre-core.rkt +++ b/racket/prologos/sre-core.rkt @@ -327,10 +327,15 @@ ;; Test distributivity: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) ;; Requires meet-fn. Returns axiom-untested if no meet available. -(define (test-distributive domain samples meet-fn) +;; +;; SRE Track 2I Phase 4 (2026-05-06): the relation keyword selects the +;; matching join from the merge-registry so the check stays inside ONE +;; lattice. Without it, a subtype-meet was paired with the equality-join, +;; mixing lattices and refuting distributivity for purely structural reasons. +(define (test-distributive domain samples meet-fn #:relation [relation 'equality]) (if (not meet-fn) axiom-untested - (let ([join ((sre-domain-merge-registry domain) 'equality)]) + (let ([join ((sre-domain-merge-registry domain) relation)]) (for/fold ([status (axiom-confirmed 0)]) ([a (in-list samples)] #:break (axiom-refuted? status)) @@ -391,11 +396,14 @@ #:transparent) ;; Detailed SD∨: a ⊔ b = a ⊔ c ⇒ a ⊔ b = a ⊔ (b ⊓ c) -(define (test-sd-vee/detailed domain samples meet-fn) +;; +;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the matching join +;; so the SD check stays inside one lattice. See test-distributive. +(define (test-sd-vee/detailed domain samples meet-fn #:relation [relation 'equality]) (cond [(not meet-fn) (sd-evidence 'untested 0 0 0 #f)] [else - (define join ((sre-domain-merge-registry domain) 'equality)) + (define join ((sre-domain-merge-registry domain) relation)) (let/ec return (define-values (total fired held) (for*/fold ([t 0] [f 0] [h 0]) @@ -421,11 +429,14 @@ (sd-evidence 'confirmed total fired held #f))])) ;; Detailed SD∧ (dual): a ⊓ b = a ⊓ c ⇒ a ⊓ b = a ⊓ (b ⊔ c) -(define (test-sd-wedge/detailed domain samples meet-fn) +;; +;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the matching join, +;; mirroring test-sd-vee/detailed. +(define (test-sd-wedge/detailed domain samples meet-fn #:relation [relation 'equality]) (cond [(not meet-fn) (sd-evidence 'untested 0 0 0 #f)] [else - (define join ((sre-domain-merge-registry domain) 'equality)) + (define join ((sre-domain-merge-registry domain) relation)) (let/ec return (define-values (total fired held) (for*/fold ([t 0] [f 0] [h 0]) @@ -454,16 +465,16 @@ ;; ------------------------------------------------------------------------ ;; Test SD∨: a ⊔ b = a ⊔ c ⇒ a ⊔ b = a ⊔ (b ⊓ c) -(define (test-sd-vee domain samples meet-fn) - (define ev (test-sd-vee/detailed domain samples meet-fn)) +(define (test-sd-vee domain samples meet-fn #:relation [relation 'equality]) + (define ev (test-sd-vee/detailed domain samples meet-fn #:relation relation)) (case (sd-evidence-status ev) [(confirmed) (axiom-confirmed (sd-evidence-total-checked ev))] [(refuted) (axiom-refuted (sd-evidence-witness ev))] [(untested) axiom-untested])) ;; Test SD∧ (dual of SD∨): a ⊓ b = a ⊓ c ⇒ a ⊓ b = a ⊓ (b ⊔ c) -(define (test-sd-wedge domain samples meet-fn) - (define ev (test-sd-wedge/detailed domain samples meet-fn)) +(define (test-sd-wedge domain samples meet-fn #:relation [relation 'equality]) + (define ev (test-sd-wedge/detailed domain samples meet-fn #:relation relation)) (case (sd-evidence-status ev) [(confirmed) (axiom-confirmed (sd-evidence-total-checked ev))] [(refuted) (axiom-refuted (sd-evidence-witness ev))] @@ -501,18 +512,21 @@ (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)) props-2)) ;; Track 2I: SD∨ and SD∧ (require meet-fn; otherwise untested) (define props-4 (if meet-fn (update-property props-3 'sd-vee - (test-sd-vee domain samples meet-fn)) + (test-sd-vee domain samples meet-fn + #:relation relation-name)) props-3)) (define props-5 (if meet-fn (update-property props-4 'sd-wedge - (test-sd-wedge domain samples meet-fn)) + (test-sd-wedge domain samples meet-fn + #:relation relation-name)) props-4)) props-5) diff --git a/racket/prologos/sre-property-sweep.rkt b/racket/prologos/sre-property-sweep.rkt index 7445b325b..1c6936855 100644 --- a/racket/prologos/sre-property-sweep.rkt +++ b/racket/prologos/sre-property-sweep.rkt @@ -91,11 +91,11 @@ (define meet-fn (sre-domain-meet domain rel)) (list (sd-finding domain-name rel 'distributive sample-count - (test-distributive domain samples meet-fn)) + (test-distributive domain samples meet-fn #:relation rel)) (sd-finding domain-name rel 'sd-vee sample-count - (test-sd-vee/detailed domain samples meet-fn)) + (test-sd-vee/detailed domain samples meet-fn #:relation rel)) (sd-finding domain-name rel 'sd-wedge sample-count - (test-sd-wedge/detailed domain samples meet-fn)))))) + (test-sd-wedge/detailed domain samples meet-fn #:relation rel)))))) ;; ======================================================================== ;; format-sd-findings From bce42aa75204416963b2b8dcdb8abd9cba3ebb64 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 6 May 2026 02:05:25 +0000 Subject: [PATCH 2/4] sre/track2i tests: use check-not-false with memq 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. --- racket/prologos/tests/test-sre-sd-properties.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/racket/prologos/tests/test-sre-sd-properties.rkt b/racket/prologos/tests/test-sre-sd-properties.rkt index 78450434b..c4b35d796 100644 --- a/racket/prologos/tests/test-sre-sd-properties.rkt +++ b/racket/prologos/tests/test-sre-sd-properties.rkt @@ -91,8 +91,8 @@ (for ([f (in-list phase3-findings)]) (check-true (sd-finding? f)) (check-eq? (sd-finding-domain-name f) 'type) - (check-true (memq (sd-finding-relation f) '(equality subtype))) - (check-true (memq (sd-finding-property f) '(distributive sd-vee sd-wedge))) + (check-not-false (memq (sd-finding-relation f) '(equality subtype))) + (check-not-false (memq (sd-finding-property f) '(distributive sd-vee sd-wedge))) (check-true (positive? (sd-finding-sample-count f))))) (test-case "Phase 3: distributive findings carry axiom-*; SD findings carry sd-evidence" From ea0e4fb3e3368e793dfd23db7b67cb5d9cb07991 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 6 May 2026 05:22:52 +0000 Subject: [PATCH 3/4] sre/track2i: thread #:relation through join-axiom checks (PR #59 review) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- racket/prologos/sre-core.rkt | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/racket/prologos/sre-core.rkt b/racket/prologos/sre-core.rkt index 79937853a..20b8f4203 100644 --- a/racket/prologos/sre-core.rkt +++ b/racket/prologos/sre-core.rkt @@ -285,9 +285,13 @@ (define axiom-untested 'axiom-untested) ;; Test commutativity of join: a ⊔ b = b ⊔ a -(define (test-commutative-join domain samples) +;; +;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the join from +;; merge-registry so axioms inferred under a non-equality relation stay +;; in that relation's lattice. Default 'equality preserves prior callers. +(define (test-commutative-join domain samples #:relation [relation 'equality]) (define merge-fn (sre-domain-merge-registry domain)) - (define join (merge-fn 'equality)) ;; equality merge = lattice join + (define join (merge-fn relation)) ;; merge under the requested relation (for/fold ([status (axiom-confirmed 0)]) ([i (in-range (length samples))] [a (in-list samples)] @@ -300,8 +304,8 @@ (axiom-refuted (list a b)))))) ;; Test associativity of join: (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c) -(define (test-associative-join domain samples) - (define join ((sre-domain-merge-registry domain) 'equality)) +(define (test-associative-join domain samples #:relation [relation 'equality]) + (define join ((sre-domain-merge-registry domain) relation)) (for/fold ([status (axiom-confirmed 0)]) ([a (in-list samples)] #:break (axiom-refuted? status)) @@ -316,8 +320,8 @@ (axiom-refuted (list a b c))))))) ;; Test idempotence of join: a ⊔ a = a -(define (test-idempotent-join domain samples) - (define join ((sre-domain-merge-registry domain) 'equality)) +(define (test-idempotent-join domain samples #:relation [relation 'equality]) + (define join ((sre-domain-merge-registry domain) relation)) (for/fold ([status (axiom-confirmed 0)]) ([a (in-list samples)] #:break (axiom-refuted? status)) @@ -502,13 +506,16 @@ (define props-0 (update-property declared 'commutative-join - (test-commutative-join domain samples))) + (test-commutative-join domain samples + #:relation relation-name))) (define props-1 (update-property props-0 'associative-join - (test-associative-join domain samples))) + (test-associative-join domain samples + #:relation relation-name))) (define props-2 (update-property props-1 'idempotent-join - (test-idempotent-join domain samples))) + (test-idempotent-join domain samples + #:relation relation-name))) (define props-3 (if meet-fn (update-property props-2 'distributive From f8a88fd007e2e84c5d72929bc070d8edcd0746bb Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 6 May 2026 05:29:21 +0000 Subject: [PATCH 4/4] sre/track2i tests: cover #:relation 'subtype contract (PR #59 review) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- racket/prologos/tests/test-sre-algebraic.rkt | 29 +++++++++++++++++++ .../prologos/tests/test-sre-sd-properties.rkt | 28 ++++++++++++++++++ 2 files changed, 57 insertions(+) diff --git a/racket/prologos/tests/test-sre-algebraic.rkt b/racket/prologos/tests/test-sre-algebraic.rkt index 758f033ee..7b8bb4cc7 100644 --- a/racket/prologos/tests/test-sre-algebraic.rkt +++ b/racket/prologos/tests/test-sre-algebraic.rkt @@ -127,6 +127,35 @@ (define result (test-idempotent-join td type-samples)) (check-true (axiom-confirmed? result))) +;; ---------------------------------------------------------------------- +;; Phase 4 (2026-05-06): join-axiom tests under #:relation 'subtype. +;; +;; The three join-axiom tests gained a #:relation keyword so that a caller +;; like `infer-domain-properties` can compute axioms in the relation's own +;; lattice. These tests lock in the contract that the keyword routes to the +;; subtype-merge from the domain's merge-registry; a regression that +;; reintroduced hardcoded 'equality would still pass for these samples +;; because the subtype merge happens to also be commutative/associative/ +;; idempotent on this set, but the explicit subtype assertion documents +;; the behavior the review surfaced. +;; ---------------------------------------------------------------------- + +(test-case "inference: commutative-join confirmed for type domain under #:relation 'subtype" + (define td (lookup-domain 'type)) + (define result (test-commutative-join td type-samples #:relation 'subtype)) + (check-true (axiom-confirmed? result)) + (check-true (> (axiom-confirmed-count result) 0))) + +(test-case "inference: associative-join confirmed for type domain under #:relation 'subtype" + (define td (lookup-domain 'type)) + (define result (test-associative-join td type-samples #:relation 'subtype)) + (check-true (axiom-confirmed? result))) + +(test-case "inference: idempotent-join confirmed for type domain under #:relation 'subtype" + (define td (lookup-domain 'type)) + (define result (test-idempotent-join td type-samples #:relation 'subtype)) + (check-true (axiom-confirmed? result))) + (test-case "inference: distributive CONFIRMED for type domain (post-Phase-3c)" ;; HISTORY: Pre-Phase-3c (Track 2I, 2026-04-30) this test asserted REFUTED. ;; That finding was an artifact of `current-lattice-subtype-fn` being installed diff --git a/racket/prologos/tests/test-sre-sd-properties.rkt b/racket/prologos/tests/test-sre-sd-properties.rkt index c4b35d796..d6cfc8f59 100644 --- a/racket/prologos/tests/test-sre-sd-properties.rkt +++ b/racket/prologos/tests/test-sre-sd-properties.rkt @@ -168,3 +168,31 @@ (check-true (positive? total)) (check-true (<= 0 fired total)) (check-true (<= 0 held fired))))) + +;; ============================================================================ +;; Phase 4 (2026-05-06): infer-domain-properties end-to-end under 'subtype +;; ============================================================================ +;; Integration regression for the lattice-mixing bug PR #59 review surfaced. +;; `infer-domain-properties` is parametrised on #:relation; after Phase 4 it +;; threads that through to all six axiom tests. With #:relation 'subtype + +;; the subtype-aware meet, every axiom should resolve to prop-confirmed for +;; the type domain (Track 2H declared subtype distributive + +;; has-pseudo-complement → distributive ⇒ SD∨ ∧ SD∧). +;; +;; If a future change reintroduces a hardcoded 'equality join lookup in any +;; of the eight functions involved, this test will refute the corresponding +;; property under subtype while leaving the equality-only suites green. + +(define subtype-meet-fn + (sre-domain-meet type-domain-for-sweep 'subtype)) + +(test-case "Phase 4: infer-domain-properties under #:relation 'subtype confirms all axioms" + (define props + (infer-domain-properties type-domain-for-sweep + realistic-type-atoms + #:meet-fn subtype-meet-fn + #:relation 'subtype)) + (for ([axiom (in-list '(commutative-join associative-join idempotent-join + distributive sd-vee sd-wedge))]) + (check-eq? (hash-ref props axiom) prop-confirmed + (format "type domain × subtype: ~a should be prop-confirmed" axiom))))