Notification subscriptions #87
Open
pgherveou wants to merge 26 commits into
Open
Conversation
pgherveou
commented
May 15, 2026
Introduces a `Notifications` trait that carries the existing
`push_notification` (moved from `System`, wire id 4 preserved) plus two
new methods:
- `push_subscribe(rule)` — register a `(signer, topic)` whitelist
rule so the user is woken up by a push
whenever a matching signed statement
appears on the Statement Store.
- `push_unsubscribe(rule)` — remove a previously registered rule.
The methods are wired through to the host's push backend (the
backend-mediated v2 design); the product never sees push tokens.
Both calls are idempotent and gated by
`DevicePermission::Notifications`.
Wire ids: `push_subscribe = 134`, `push_unsubscribe = 136`.
`push_notification` keeps `request_id = 4` so the move is wire-stable.
- Change HostPushListRulesRequest from unit struct to empty braced struct so the codegen can handle it. - Rewrite rule-method TS examples to use literal default requests instead of variable references, matching the playground codegen's expectation of extractable JSON.
filvecchiato
force-pushed
the
notification-subscriptions
branch
from
7c2e02f to
8788def
Compare
filvecchiato
approved these changes
May 15, 2026
Collaborator
filvecchiato
left a comment
filvecchiato
left a comment
There was a problem hiding this comment.
OK this is good to go, I suggest merging this before RFC0019 since I add scheduled_at to the pushNotificationRequest struct
…tions # Conflicts: # docs/rfcs/_index.md # rust/crates/truapi/src/api/notifications.rs # rust/crates/truapi/src/api/system.rs # rust/crates/truapi/src/v01/notifications.rs # rust/crates/truapi/src/v01/system.rs # rust/crates/truapi/src/versioned/notifications.rs
filvecchiato
approved these changes
May 19, 2026
valentunn
reviewed
May 19, 2026
|
|
||
| ### Worked example: festival announcements | ||
|
|
||
| A conference product publishes festival-wide announcements as signed statements on a well-known topic, signed with the product's own identity key (`pkProduct`). When the user taps "notify me about announcements," the subscriber app calls `push_add_rules({ topics: [announcements_topic] })`. The host injects `pkProduct` as the signer when relaying to the backend, so from that point on the user is woken up for new announcements even with the product closed: |
Contributor
There was a problem hiding this comment.
How does the user's host know about pkProduct? Product instance running on user device and product instance running on admin device are two separate instances.
Maybe we should allow product to specify pkProduct in add_rules?
Overall it seems like this "worked example" is mixing motivation and implementation show-case which is very confusing to me
…d add optional signer to rule requests Address review feedback: - Replace BackendUnavailable with NotificationSystemUnavailable(String) so the error variant does not leak implementation details; the string payload lets hosts describe why the system is unavailable. - Add `signer: Option<ProductAccountId>` to HostPushAddRulesRequest, HostPushRemoveRulesRequest, and HostPushSetRulesRequest so a product can subscribe to statements from a different product's identity.
Authors now create unnumbered `docs/rfcs/<slug>.md` files. On merge to main the new `number-rfc.yml` workflow assigns the next sequential number, renames the file, and appends it to `_index.md`. Updated CONTRIBUTING.md, PR template, and RFC template accordingly.
This reverts commit 792cd8e.
pgherveou
commented
May 25, 2026
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
Adds the 2-coin special case of multi-coin exact subset-sum (Quint selectExactCoverDeterministic). Nested-loop scan, O(n^2) over the coin Vec, returns Some((k1, k2)) where both keys are distinct, Available, in purse p, and coin_value(exp_k1) + coin_value(exp_k2) exactly equals the requested amount. This is the first multi-coin extension of tier-1. It covers practically-important cases where single-coin tier-1 fires None but two coins happen to sum exactly (e.g. amount = 11, coins of value 6 + 5). The full powerset enumeration over arbitrary subset sizes remains task #87 — adding 3-coin, then iterative-deepening, follows the same Vec-scan pattern with proportionally more nested loops. The None postcondition is intentionally weak (`true`) for now: proving "no 2-coin subset sums to amount" requires the contrapositive of the existential, which adds significant proof obligations. Sharper None postconditions can land incrementally. 160 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
The None branch was `true` (vacuous) — useful as a witness but unusable for composition. Sharpens it to the operationally-meaningful quantifier: no two distinct Vec indices i1 != i2 form a pair where both coins are Available in p and their values sum to amount. The dedup invariant (n) over (purse, idx) means Vec-index distinctness implies key distinctness, so this is equivalent to the dom-based "no two distinct keys" claim. Stated over Vec indices for cleaner trigger discipline (let-binding trigger pattern). The proof discharges via accumulated loop invariants on both outer and inner loops; no extra proof block needed. 209 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
find_three_coin_exact_cover: triple-nested loop searching for distinct coin triples (k1, k2, k3) whose values sum exactly to amount. Same structural pattern as find_two_coin_exact_cover, one dimension deeper: - Outer accumulator: no triple with first index < i works. - Middle accumulator: no triple (i, j1, j3) with j1 < j works. - Inner accumulator: no triple (i, j, k2) with k2 < k works. When all three loops exhaust, the postcondition's forall|i1, i2, i3| distinct ==> sum != amount follows. The 2-coin → 3-coin extension was first-attempt clean — the pattern generalizes directly. Further extension to 4-coin, 5-coin, ... is the same shape with proportionally more nesting. Task #87 is partially closed: 1-coin (find_exact_single_coin) + 2-coin (find_two_coin_exact_cover) + 3-coin (this commit) all ship with sharp None. Full N-coin powerset via bitmask enumeration over the first K Available coins is still open as the "real" general form. 253 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
find_four_coin_exact_cover: quadruple-nested loop with four-level accumulator pattern. Same structural shape as 2/3-coin, one more dimension. The pattern scales — N-coin extension is mechanical proportional growth with the same proof skeleton. Sharp None postcondition over all quadruples of pairwise-distinct Vec indices. 258 verified, 0 errors. Task #87 progress: 1/2/3/4-coin all ship with sharp None.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
…Cover Practical multi-coin selector. Tries 1-, 2-, 3-, 4-coin exact covers in order and returns the first hit as a tagged enum (SubsetSumCover). The None branch carries the CONJOINED sharp postconditions from all four primitives — for any subset of size <=4 in the purse, no such subset sums to amount. The Vec-of-coins API rejected in favor of a tagged enum keeps the size-specific postcondition shape clean per variant. This closes the practically-relevant slice of #87. The remaining open piece — N-coin subset-sum for arbitrary N via bitmask enumeration — would extend coverage to larger subsets at the cost of new spec scaffolding (sum_by_mask, witness extraction). Size 1-4 covers essentially every realistic transfer in a real wallet. 259 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
…rp None The None branch postcondition gets the same accumulator-pattern forall-no-pair-works claim as find_two_coin_exact_cover. Outer accumulator covers all coin indices < i; inner accumulator covers all entry indices < k for current i. 259 verified, 0 errors. First try clean — same pattern as the multi-coin extensions in #87.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
find_two_coin_one_entry_cover and find_one_coin_two_entry_cover — both with sharp None postconditions. Same accumulator pattern as the multi-coin #87 series, with the dimensions split between coin and entry Vecs. Each landed first-try clean. Combined with the strengthened find_coin_entry_exact_cover (1c+1e with sharp None) shipped earlier, we now have all coin/entry covers of total size 2 and 3 with full sharp None. 267 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
…er enum Practical tier-3 entry-supplemented cover selector. Tries all 8 sub-primitives (1-coin, 1-entry, 2-coin, 1c+1e, 2-entry, 3-coin, 2c+1e, 1c+2e) in size + complexity order and returns the first hit as a tagged Tier3Cover enum. The None branch is the CONJUNCTION of all 8 underlying sharp Nones — no subset of size 1, 2, or 3 (any coin/entry split) in the purse sums to amount. This closes the practical slice of #88. Higher-order powerset (arbitrary coin/entry subsets) remains open as the same kind of diminishing-marginal-value extension noted for #87. Sizes 1, 2, 3 cover the realistic cases. 273 verified, 0 errors.
pgherveou
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
4 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.
Summary
Adds four host calls that let a product manage its push-notification rules, mirroring the rule endpoints in the v2 push backend spec:
push_add_rules: register one or more topics the user wants to be woken up forpush_remove_rules: drop one or more topicspush_list_rules: snapshot the rules currently active for this productpush_set_rules: atomic replace of the full rule setMotivation
The v2 push design delivers a push when a signed statement matching a user-whitelisted
(signer, topic)pair appears on the Statement Store. TrUAPI needs a primitive for products to manipulate that whitelist.