test(comms): pin dmChannelName properties and DM two-party read scope (RIG-3535) - #1136
Merged
trunk-io[bot] merged 1 commit intoSep 12, 2026
Conversation
… (RIG-3535)
Adds an untagged table test for `dmChannelName` and two pgtest lifecycle cases.
The untagged test moves two already-proven properties to the cheapest tier:
order independence, and injectivity across the `:` separator. The injectivity
case is the confidentiality-relevant one — a hyphen delimiter would derive the
same name for the distinct pairs {a, b--c} and {a--b, c}, cross-adding members
into a same-owner private DM.
The pgtest cases cover both parties posting and reading each other's messages,
and a third same-owner agent reading nothing from a DM it is not a member of.
The third-party case is canary-ordered: a real party is proven to read the post
before the outsider's empty read is asserted, so an undelivered post cannot pass
it vacuously.
Mutation-verified, each against production code:
- dropping the sort swap in `dmChannelName` fails the untagged test
- switching the separator to `--` fails it on the injectivity assertion
- weakening the ListMessages membership join to any-member fails the
third-party case
Co-authored-by: Matt Wilkinson <matt@rigel.build>
This was referenced Sep 12, 2026
Merged
rigel-mintaka
added this pull request to stack #1124
September 12, 2026 02:19
rigel-mintaka
marked this pull request as ready for review
September 12, 2026 02:20
|
Compass engineering docs preview: https://compass-comms-rig3535-dm-lif.compass-eng-docs.pages.dev Deployed from |
mattwilkinsonn
approved these changes
Sep 12, 2026
|
This pull request was merged into |
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
2 participants
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.
This PR is part of a stack containing 4 PRs:
mainAdds an untagged table test for
dmChannelNameand two pgtest lifecycle cases.The untagged test moves two already-proven properties to the cheapest tier:
order independence, and injectivity across the
:separator. The injectivitycase is the confidentiality-relevant one — a hyphen delimiter would derive the
same name for the distinct pairs {a, b--c} and {a--b, c}, cross-adding members
into a same-owner private DM.
The pgtest cases cover both parties posting and reading each other's messages,
and a third same-owner agent reading nothing from a DM it is not a member of.
The third-party case is canary-ordered: a real party is proven to read the post
before the outsider's empty read is asserted, so an undelivered post cannot pass
it vacuously.
Mutation-verified, each against production code:
dmChannelNamefails the untagged test--fails it on the injectivity assertionthird-party case
Co-authored-by: Matt Wilkinson matt@rigel.build