Skip to content

sre/track2i: Phase 4 — relation-aware join in distributive/SD checks #59

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kumavis wants to merge 4 commits into
base: main
Choose a base branch
from
+105 −27
Open

sre/track2i: Phase 4 — relation-aware join in distributive/SD checks #59

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e30b2dd
sre/track2i: Phase 4 — relation-aware join in distributive/SD checks
claude May 6, 2026
bce42aa
sre/track2i tests: use check-not-false with memq
claude May 6, 2026
ea0e4fb
sre/track2i: thread #:relation through join-axiom checks (PR #59 review)
claude May 6, 2026
f8a88fd
sre/track2i tests: cover #:relation 'subtype contract (PR #59 review)
claude May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 27 additions & 13 deletions racket/prologos/sre-core.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -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])
Expand All @@ -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])
Expand Down Expand Up @@ -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))]
Expand Down Expand Up @@ -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))
Comment on lines 519 to +523

@kumavis kumavis May 6, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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)

Expand Down
6 changes: 3 additions & 3 deletions racket/prologos/sre-property-sweep.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions racket/prologos/tests/test-sre-sd-properties.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Loading