Notification

Atom grounded on Final Critique 11 — 2026-11-05 at 917cc95 9 invariants Alloy model buggy twin ×1 regulated · via 2 composers composed by 2

Derived card — generated from the corpus (status line, invariant headers, sibling formal-model files, Composes edges). The specification below is canonical. composition graph →

Table of contents

Notification

Summary

Notification records whether a single piece of information was accepted by the transport for a single recipient. Where Subscription records who wants to know about a class of events, Notification records the outcome of one delivery. It creates a permanent, unchangeable record of a delivery attempt and tracks it to one of three end states: Delivered (the transport layer confirmed receipt), Failed (the transport returned a definite error), or Expired (the delivery window ran out with no recorded outcome). These are kept as three distinct states because each answers a different question and is handled by a different part of the system — the delivery layer, the failure handler, the expiry scheduler. The pattern does not decide who should be notified or how to reach them; by the time it is asked to create a record, the recipient and the content are already settled. Nothing is ever deleted, so the full delivery history of any notification is always recoverable. This is what underlies delivery audit trails in regulated settings, and it is the substrate for retry logic, which records each retry as a new notification rather than altering the failed one.

Intent

WHY

A notification is a promise to tell somebody something, and the interesting part is not the telling — it is the record of whether it happened. Systems that skip this concept end up asking their transport layer what happened weeks ago, which is a question no transport layer can answer. The atom holds the delivery record: who it was for, what it said, when it was made, and exactly one outcome — reached, failed, or ran out of time. It sends nothing. It does not know what a webhook is, does not retry, does not decide whether a bounced email is a failure or an expiry. What it guarantees is that every attempt is one record with one terminal answer and a timestamp, so did we tell them is answered from the database rather than from a log nobody kept.

Structure

Identity model

Identity 1: The atom MUST identify a notification by the notification id.
Identity 2: The host MUST allocate a notification id at the atom's seam.
Deleted: Identity 3. Execution Contract Logic confinement 3 owns it.
Identity 4: The business caller MUST NOT supply a notification id.
Identity 5: The atom MUST NOT reuse a notification id.
Identity 6: The atom MUST NOT identify a notification by the recipient reference with the payload.
Identity 7: Two notifications carrying one recipient reference and one payload MUST carry two notification ids.

NOTE: watch the allocation ban (Identity 3).

Term notification: one delivery record — one recipient, one payload, one outcome.

Term notification id: the opaque string naming one notification — a Notification Id; malformed where it is no string.

Term recipient reference: the opaque string naming who the notification is for — a Recipient Reference; compared by equality and never interpreted; malformed where it is no string.

Term payload: the opaque content the notification carries — a Payload; stored and returned unchanged.

Term seam: the atom’s I/O boundary as Execution Contract Logic confinement 14 declares it; the host injects the clock reading and the notification id here.

Term transition: the evaluation of one call against the notification records, as Execution Contract Logic confinement 14 declares it.

Term business caller: the business caller per Execution Contract Logic confinement 14.

Term now: the deployment’s clock reading at the call — a Now, as Execution Contract Logic confinement 11 declares it.

NOTE: watch the seam citation (Term seam, Term transition, Term business caller).

State

State 1: EVERY notification MUST stand in EXACTLY ONE OF pending, delivered, failed, expired.
State 2: EVERY notification MUST carry notification id, recipient reference, payload, creation instant and status.
State 3: A delivered notification MUST carry delivery instant.
State 4: A failed notification MUST carry failure instant.
State 5: An expired notification MUST carry lapse instant.
State 6: A pending notification MUST NOT carry a terminal stamp.
State 7: [Create] MUST stamp creation instant from the injected now.
State 8: A terminal transition MUST stamp the transition's terminal stamp from the injected now.
State 9: The atom MUST NOT offer a transition out of a terminal status.
State 10: The atom MUST NOT delete a notification.
State 11: The atom MUST NOT hold a transport.
State 12: The atom MUST NOT hold a retry.

Term status: pending

delivered

failed

expired — the Status field’s four values: awaiting an outcome, reached, ended as failed, or ended as expired.

Term terminal stamp: delivery instant

failure instant

lapse instant — the one stamp a terminal status carries.

Term creation instant: the instant the notification was recorded — a Creation Instant.

Term notification set: the notifications the database holds.

Capability requirement

Capability requirement 1: The deployment MUST supply now at the seam.
Capability requirement 4: The deployment MUST supply the notification records PER Execution Contract Database 1 through 4, Execution Contract Read 1 through 4 and Execution Contract Refusal 1.
Capability requirement 5: The deployment MAY declare the string cap PER Execution Contract Input 2.
Capability requirement 6: The deployment MUST NOT change the string cap for the life of the instance.
Capability requirement 7: The deployment MUST declare which composing patterns the deployment wired in PER Execution Contract Conformance 9.
Capability requirement 8: The deployment MUST declare the deployment's fail-versus-expire policy.
Capability requirement 9: The deployment MUST supply at the seam a notification id no notification has carried PER Execution Contract Logic confinement 3.
Deleted: Capability requirement 2. Execution Contract Logic confinement 7 owns it.
Deleted: Capability requirement 3. Execution Contract Logic confinement 7 owns it.
Deleted: Clock semantics 1. Execution Contract Logic confinement 7 owns it.
Deleted: Clock semantics 2. Execution Contract Logic confinement 7 owns it.
Deleted: Clock semantics 3. Non-goal 16 owns it.

NOTE: watch the deployment’s composition note (Capability requirement 7).

Operations

create(recipient_ref, payload)
  answers notification_id
  refuses invalid-request | storage-failure

deliver(notification_id)
  answers ok
  refuses not-known | not-pending | storage-failure

fail(notification_id)
  answers ok
  refuses not-known | not-pending | storage-failure

expire(notification_id)
  answers ok
  refuses not-known | not-pending | storage-failure

status_of(notification_id)
  answers notification | not-known

pending_for(recipient_ref)
  answers notification_ids

NOTE: open 2026-10-21-f — the success arm ok and the answer arm notification_ids resolve to no declaration on the page.

Operation 1: [Create] MUST record EXACTLY ONE notification per successful call.
Operation 2: [Create] MUST stand the notification in pending.
Operation 3: [Create] MUST answer notification id.
Operation 4: IF recipient reference EQUALS blank THEN [Create] MUST answer invalid-request.
Operation 5: [Create] MUST accept an empty payload.
Operation 6: The atom MUST NOT evaluate a payload.
Operation 7: IF the database refuses the write THEN [Create] MUST answer storage-failure.
Operation 8: IF no notification EXISTS for the notification id THEN a terminal transition MUST answer not-known.
Operation 9: IF the notification's status DOES NOT EQUAL pending THEN a terminal transition MUST answer not-pending.
Operation 10: [Deliver] MUST stand the notification in delivered.
Operation 11: [Fail] MUST stand the notification in failed.
Operation 12: [Expire] MUST stand the notification in expired.
Operation 13: [Expire] MUST NOT require a delivery attempt.
Operation 14: The atom MUST NOT choose between fail and expire.
Operation 14a: The atom MUST NOT hold a delivery window.
Operation 14b: A composing pattern MUST own the delivery window an expiry answers to.
Operation 15: IF the database refuses the write THEN a terminal transition MUST answer storage-failure.
Operation 16: A refused call MUST leave the notification as the call found the notification.
Operation 17: [Status Of] MUST answer the notification's stored fields.
Operation 18: IF no notification EXISTS for the notification id THEN [Status Of] MUST answer not-known.
Operation 18b: IF a notification id is malformed THEN [Status Of] MUST answer not-known (Execution Contract Query 1, Query 5).
Operation 19: [Pending For] MUST answer the notification id of EVERY pending notification carrying the recipient reference.
Operation 20: [Pending For] MUST NOT answer a terminal notification's notification id.
Deleted: Operation 21. Execution Contract Read 5 owns it.
Operation 22: [Status Of] MUST NOT write.
Operation 23: [Pending For] MUST NOT write.
Deleted: Operation 24. Capability requirement 1 owns it.
Deleted: Operation 25. Execution Contract Logic confinement 3 owns it.
Deleted: Operation 26. Execution Contract Logic confinement 3 owns it.
Deleted: Operation 27. Execution Contract Read 1 owns it.
Deleted: Operation 28. Execution Contract Read 1 owns it: after the read, every refusal rule of [Create] answers invalid-request.
Deleted: Operation 29. Execution Contract Refusal 1 owns it.
Deleted: Operation 30. Execution Contract Input 4 owns it.
Operation 31: IF a recipient reference is malformed THEN [Create] MUST answer invalid-request (Execution Contract Input 1).
Operation 32: IF a notification id is malformed THEN a terminal transition MUST answer not-known (Execution Contract Input 1).

NOTE: watch the required input no rule records (Operation 30).

NOTE: watch the untyped input (Operation 31, Operation 32, Term notification id, Term recipient reference).

NOTE: the ids a Pending For answers come in the order Execution Contract Read 5 states; no rule of this atom names another (Operation 19).

NOTE: watch the order an atom forbids (Operation 21).

Term terminal transition: a Deliver, a Fail or an Expire call — the three that end a notification, sharing one precondition pair.

Term pending at an instant: the instant DOES NOT PRECEDE creation instant, and the notification carries no terminal stamp or the instant PRECEDES the terminal stamp the notification carries — the reconstruction an auditor runs over stored fields, never over status, which carries the present rather than the past.

The case space, and the rule that owns each case:

Call	Case	Answer	Effect on the notification records
Create	recipient present, database accepts	notification id	one notification lands in Pending (Operation 1, Operation 2, Execution Contract Input 4)
Create	blank or malformed recipient, or over the cap	Invalid Request	none (Operation 4, Operation 31, String 6)
Create	empty payload	notification id	one notification lands — the payload is the caller’s business (Operation 5, Operation 6)
Deliver	notification is pending	ok	Pending → Delivered, delivery instant stamped (Operation 10, State 8)
Fail	notification is pending	ok	Pending → Failed, failure instant stamped (Operation 11)
Expire	notification is pending, attempted or not	ok	Pending → Expired, lapse instant stamped (Operation 12, Operation 13)
any terminal transition	notification already terminal	Not Pending	none — including a second Deliver (Operation 9)
any terminal transition	id names nothing, or is malformed	Not Known	none (Operation 8, Operation 32)
any write	database refuses	Storage Failure	none (Operation 7, Operation 15, Operation 16)
Status Of	id names a notification	its stored fields	none — the call reads (Operation 17, Operation 22)
Status Of	id names nothing, or is malformed	not-known	none (Operation 18, Operation 18b)
Pending For	recipient has pending notifications	their ids, in Execution Contract Read 5’s order	none (Operation 19, Execution Contract Read 5)
Pending For	recipient has none, or only terminal ones	empty list	none (Operation 20)
Pending For	over-length or blank recipient	empty list	none — a read with a bad argument has a correct answer (String 8, String 9)

Invariants

Invariant 1 — Notification immutability.

Invariant 1.1: A recorded notification's notification id, recipient reference, payload and creation instant MUST NOT change.
Invariant 1.2: A landed terminal stamp MUST NOT change.

Invariant 2 — Status monotonicity.

Deleted: Invariant 2.1. State 1 owns it.
Invariant 2.2: A status MUST NOT move to pending from a terminal status.
Invariant 2.3: A status MUST NOT move between two terminal statuses.
Invariant 2.4: A notification MUST read as pending at an instant ONLY IF the notification is pending at an instant.

Invariant 3 — Terminal states are exclusive.

Invariant 3.1: A notification whose status DOES NOT EQUAL pending MUST carry EXACTLY ONE terminal stamp.
Deleted: Invariant 3.2. State 6 owns it.

Invariant 4 — Terminal timestamps match status.

Deleted: Invariant 4.1. State 3 owns it.
Invariant 4.2: A notification carrying delivery instant MUST stand in delivered.
Deleted: Invariant 4.3. State 4 owns it.
Invariant 4.4: A notification carrying failure instant MUST stand in failed.
Deleted: Invariant 4.5. State 5 owns it.
Invariant 4.6: A notification carrying lapse instant MUST stand in expired.

Invariant 5 — Id stability.

Invariant 5.1: [Create] MUST set the notification id.
Deleted: Invariant 5.2. Invariant 1.1 owns it.

Invariant 6 — No id reuse.

Invariant 6.1: Two notifications MUST NOT share a notification id.

Invariant 7 — Pending query excludes terminals.
```
Deleted: Invariant 7.1. Operation 20 owns it.
```

Invariant 8 — Timestamp ordering.

Invariant 8.1: IF delivery instant DOES NOT EQUAL blank THEN delivery instant MUST NOT PRECEDE creation instant.
Invariant 8.2: IF failure instant DOES NOT EQUAL blank THEN failure instant MUST NOT PRECEDE creation instant.
Invariant 8.3: IF lapse instant DOES NOT EQUAL blank THEN lapse instant MUST NOT PRECEDE creation instant.

Invariant 9 — Notification durability.

Invariant 9.1: The atom MUST NOT delete a notification record.
Invariant 9.2: The notification set MUST NOT shrink.
Invariant 9.3: [Status Of] MUST answer a created notification's fields for the database's life.

Immutability and durability give auditability — the delivery history is the database, with no gaps. Exclusivity and the status-stamp match give the unambiguous record property — one outcome per notification, with a stable time. Monotonicity and ordering make Pending For a deterministic snapshot of what is still unresolved.

Examples

The same atom, three domains, identical mechanic.

Shared Todo — assignment notification delivery

A Notification Fanout pattern creates a notification when a task is assigned: create(dev_d, {type: "task:assigned", task_id: t1, assigned_by: manager_m}) → notif_77. The WebSocket layer pushes the payload to dev_d’s active session and calls deliver(notif_77) → Delivered. status_of(notif_77) returns status = delivered, Delivery Instant set. pending_for(dev_d) returns [].

If dev_d is offline, the push attempt produces a connection error: fail(notif_77) → Failed. The composing system may create a retry notification: create(dev_d, {same payload}) → notif_78 — a new Pending record, distinct id, independent outcome.

If neither delivery nor failure is recorded within the expiry window: expire(notif_77) → Expired. status_of(notif_77) returns Lapse Instant.

NOTE: open 2026-10-21-b — the three outcomes of notif_77 above are alternatives, which only each paragraph’s condition says.

Support queue — escalation alert

When queue 9 escalates, the fanout pattern creates one notification per subscribed supervisor: create(supervisor_s, {type: "escalation", queue: 9, ticket: t22}) → notif_33. Email delivery succeeds: deliver(notif_33) → Delivered. status_of(notif_33) returns status = delivered, Delivery Instant. Elapsed delivery time is delivered_at − created_at.

Supervisor_s later asks “was I notified about the queue-9 escalation?” — pending_for(supervisor_s) returns an empty list (nothing pending), and status_of(notif_33) returns status = delivered with Delivery Instant. The delivery record answers the question provably, from stored fields.

Compliance system — policy change

An administrator broadcasts a policy update. Three compliance officers each receive a notification: create(officer_a, {type: "policy:updated", policy_id: p7}) → notif_101, similarly for officers b and c. Officer_a’s email bounces: fail(notif_101). Officers b and c are delivered successfully. status_of(notif_101) shows Failure Instant; status_of(notif_102) and status_of(notif_103) show Delivery Instant. An operator queries pending_for for each officer — empty for all three. The notification records show: two Delivered, one Failed; the composing system creates a retry for officer_a or escalates to a secondary channel.

Rejection path — invalid create

A composing system attempts to create a notification with an empty recipient reference: create(recipient_ref: "", payload: {type: "task:assigned", task_id: "t1"}) → invalid-request. No Notification Id is issued; no record enters the database. The composing system must supply a non-empty recipient reference before the notification can be created.

Regulated adversarial scenarios

Three scenarios the notification records must survive in regulated contexts:

Regulator audit — demonstrate all notifications for a compliance event. A compliance auditor asks “show all notifications created for the policy:updated event on 2025-03-14, and whether each was delivered.” The auditor queries the notification records for notifications where creation instant falls on 2025-03-14 and the payload references the relevant policy. Status Of for each returned id shows the delivery outcome — Delivery Instant, Failure Instant, or Lapse Instant. The notification records answer provably, from stored fields; Invariants 1 and 3-4 guarantee the delivery record is complete and unambiguous.
Disputed delivery — actor claims they were not notified. Officer_a claims they received no notification of policy update p7. The investigator queries the notification records for notifications where recipient_ref = officer_a and the payload references policy_id: p7. If a record exists with Delivery Instant set, Invariant 1 (notification immutability) is the structural answer: the notification was created with that recipient and delivery was confirmed at that time. If the record shows Failure Instant or Lapse Instant, the notification records show that no delivery was recorded, and which outcome was recorded instead. The notification records are the single source of truth for what was recorded; whether the transport reached the recipient regardless is the delivery layer’s own record (External check 4).
Breach investigation — identify Pending notifications that may have exposed payload data. A security incident requires identifying all notifications that were Pending at the time of breach (2025-06-01T03:00Z) and may have carried sensitive payload data. The investigator queries for notifications where created_at ≤ 2025-06-01T03:00Z and either status = pending (still unresolved now) or the applicable terminal timestamp falls after 2025-06-01T03:00Z (meaning the notification was Pending during the breach window but has since resolved). The reconstruction logic mirrors the Subscription pattern: created_at ≤ T and (status = pending or delivered_at > T or failed_at > T or expired_at > T). Status Of for each candidate returns the current record; creation instant confirms the exposure window. The notification records answer the exposure scope question provably, from stored fields.

Generation acceptance

This atom’s acceptance is provable: an external auditor clears it from the notification records’ stored fields, with their committed versions (Execution Contract Generation acceptance 1). The audit surface is the database, not the action surface.

Conformance checks

Check 1.1: An auditor MUST read EVERY notification's notification id, recipient reference, payload, creation instant and status from the database (State 2).
Check 2.1: An auditor MUST reconstruct a notification's status at an instant from creation instant and the terminal stamp (Invariant 2.4).
Check 2.2: An auditor MUST read the reconstruction as deterministic on stored fields (Invariant 1.1, Invariant 1.2).
Check 2.3: An auditor MUST read the reconstruction's wall-clock truth as best-effort (Invariant 8.1, Execution Contract Logic confinement 7).
Check 3.1: An auditor MUST find EVERY notification whose status DOES NOT EQUAL pending carrying EXACTLY ONE terminal stamp (Invariant 3.1).
Check 3.2: An auditor MUST find no pending notification carrying a terminal stamp (State 6).
Check 4.1: An auditor MUST find EVERY terminal stamp matching the notification's status (Invariant 4.2, Invariant 4.4, Invariant 4.6).
Check 5.1: An auditor MUST find the notification set never shrinking across the notifications' committed versions (Invariant 9.1, Invariant 9.2; Execution Contract Generation acceptance 1).
Deleted: Check 6.1. Execution Contract Conformance 9 owns it.
Check 6.2: An auditor MUST find no two notifications sharing a notification id (Invariant 6.1).

Term committed version: a record as it stood at the commit that wrote it, as Execution Contract Generation acceptance 1 declares it.

External checks

External check 1: An auditor MUST read the deployment's fail-versus-expire policy from the deployment's own declaration (Operation 14, Capability requirement 8).
External check 2: An auditor MUST read a payload's retention from the composing Retention Window records (Non-goal 13).
External check 3: An auditor MUST read who created a notification from the composing Actor Identity attestations (Non-goal 11).
External check 4: An auditor MUST read the transport's own outcome from the deployment's delivery layer (Non-goal 5).
Deleted: External check 5. Execution Contract Conformance 9 owns it.

NOTE: EVERY check names the rule the check tests. External check 1 is the one that makes cross-deployment audit possible: without the declared policy, one shop’s failure instant and another’s lapse instant record the same operational event and no reader can tell.

Non-goals

Non-goal 1: The atom MUST NOT evaluate a subscription.
Non-goal 2: The atom MUST NOT choose a notification's recipient.
Non-goal 3: The atom MUST NOT retry a failed notification.
Non-goal 4: A composing pattern retrying MUST create a second notification.
Non-goal 5: The atom MUST NOT deliver a notification.
Non-goal 6: The atom MUST NOT hold a transport's mechanism.
Deleted: Non-goal 7. Execution Contract Read 5 owns it.
Non-goal 8: The atom MUST NOT record a recipient's reading.
Non-goal 9: A deployment needing a read acknowledgement MUST create a second notification for the acknowledgement.
Non-goal 10: The atom MUST NOT validate a payload.
Non-goal 11: The atom MUST NOT record who called [Create].
Non-goal 12: The atom MUST NOT deduplicate two notifications.
Non-goal 13: The atom MUST NOT purge a payload.
Non-goal 14: The atom MUST NOT gate [Create] on a caller's authority.
Non-goal 15: The atom MUST NOT expire notifications in bulk.
Non-goal 16: A deployment needing a defensible timeline MUST compose a trusted timestamping pattern.

NOTE: the owners — Subscription and Notification Fanout (Non-goal 1, Non-goal 2); Retention Window (Non-goal 13, Payload retention 3).

Where the atom breaks down: when delivered is not a single observable event — a multi-hop transport with partial acknowledgement; when the same notification must be retried in place, which this atom refuses on purpose; when the payload cannot be stored at all, which needs a reference rather than content.

Edge cases

String policy

String 1: The atom MUST compare a string input byte-exactly.
String 2: The atom MUST NOT trim a string input.
String 3: The atom MUST NOT normalize a string input.
String 4: The atom MUST NOT case-fold a string input.
Deleted: String 5. GRACE-lang Term blank owns it.
String 6: IF the recipient reference EXCEEDS the string cap THEN [Create] MUST answer invalid-request.
String 7: The business caller MUST own a recipient reference's canonical form.
String 8: [Pending For] MUST read an over-length recipient reference as matching nothing.
String 9: [Pending For] MUST read a blank recipient reference as matching nothing.

Term string cap: the bound on the recipient reference’s length, measured in Unicode code points; 256 code points where a deployment declares none; a cap of zero refuses every Create, which is the degenerate configuration a deployment owns rather than a state the atom admits.

NOTE: watch the cap’s floor (Term string cap).

Atomicity of a terminal transition

Deleted: Terminal atomicity 1. Execution Contract Database 1 owns it.
Deleted: Terminal atomicity 2. Execution Contract Database 1 and Execution Contract Database 3 own it.
Deleted: Terminal atomicity 3. Execution Contract Database 1 and Execution Contract Database 3 own it.
Deleted: Terminal atomicity 4. Execution Contract Database 2 owns it.

Bulk expiry

Bulk expiry 1: A composing pattern MUST enumerate a recipient's pending notifications.
Bulk expiry 2: A composing pattern MUST call [Expire] for EVERY notification the enumeration returns.
Bulk expiry 3: A composing pattern MUST NOT read one expiry as a deadline sweep.

NOTE: open 2026-11-05-a — Bulk expiry 1 and Bulk expiry 2 carry no condition, so as written they bind every composing pattern, not the one that expires in bulk.

Deliver persistence failure

Deliver persistence 1: A caller MUST read storage-failure from [Deliver] as the notification whose status EQUALS pending.
Deliver persistence 2: A caller MUST retry a deliver that answered storage-failure.
Deliver persistence 3: A caller MUST NOT deliver the payload a second time on that retry.
Deliver persistence 4: A high-assurance deployment MUST raise an alert on storage-failure from [Deliver].

NOTE: open 2026-10-21-g — a high-assurance deployment (Deliver persistence 4) is declared nowhere, and the alert names no receiver.

Payload retention

Payload retention 1: The atom MUST keep a payload for the database's life.
Payload retention 2: The atom MUST NOT offer a payload purge.
Payload retention 3: A deployment whose payloads carry sensitive content MUST compose Retention Window.
Payload retention 4: A composing pattern purging a payload MUST leave EVERY stored field as written.
Payload retention 5: A composing pattern MUST NOT delete a notification record.

WHY

What a composed purge can do is a shred, as Audit Trail wires one over its own cascade (Payload retention 4, Payload retention 5).

Composition notes

Deleted: Composition note 1. Capability requirement 7 owns it.
Deleted: Composition note 2. Capability requirement 8 owns it.
Composition note 3: A composing pattern MUST own who is notified.
Composition note 4: A composing pattern MUST own the transport.
Composition note 5: A composing pattern needing at-most-once notification MUST guard [Create] with Duplicate Prevention.
Composition note 6: A composing pattern MUST own a payload's retention.
Deleted: Composition note 7. Operation 14b owns it.

NOTE: composing patterns — Notification Fanout, Preference-Aware Notification Fanout.

Terms

Each [Term] marker above links to its term entry here; a term entry states what the concept is and its Kind.

Vocabulary

Term actors: the atom; the host; the transition; the deployment; a composing pattern (also: a pattern); a business caller; a caller; a recipient; an auditor; the database; a notification; a status.

Term records: notification — one delivery record, carrying notification id, recipient reference, payload, creation instant, status and, once it ends, one terminal stamp.

Term record verbs: identify, allocate, supply, reuse, carry, compare, trim, normalize, case-fold, read, stand, stamp, offer, delete, hold, record, answer, accept, leave, refuse, order, write, change, move, set, share, shrink, keep, own, evaluate, choose, retry, create, deliver, validate, deduplicate, purge, gate, expire, enumerate, call, compose, guard, declare, find, reconstruct, raise, require, precede.

Term value sets: status = pending

delivered

failed

expired. terminal stamp = delivery instant

failure instant

lapse instant.

Term bounds: string cap (the bound on the recipient reference’s length, measured in Unicode code points, 256 where a deployment declares none).

Term cadences: empty — a delivery window is the composing pattern’s (Operation 14b).

Term qualifiers: migrated — rewritten in GRACE lang v0.35 (2026-09-12).

Term terms: notification, notification id, recipient reference, payload, seam, transition, business caller, now, string cap, status, terminal stamp, creation instant, terminal transition, pending at an instant, committed version, notification set.

Create

The behavior that records a new delivery record. It assigns a fresh Notification Id (host-allocated at the seam), records Recipient Reference, Payload, and Creation Instant, and returns the Notification Id (or Invalid Request). The record enters Pending.

Kind: Operation

Deliver

The behavior that records successful delivery, transitioning a Pending notification to terminal Delivered and stamping Delivery Instant. Rejected for an unknown or malformed id (Not Known) or a non-Pending notification (Not Pending).

Kind: Operation

Fail

The behavior that records a definitive delivery failure, transitioning a Pending notification to terminal Failed and stamping Failure Instant. Same preconditions as Deliver.

Kind: Operation

Expire

The behavior that records lapse of the delivery window without an outcome, transitioning a Pending notification to terminal Expired and stamping Lapse Instant. Same preconditions as Deliver.

Kind: Operation

Status Of

The read-only query returning the full record for a Notification Id in any state, or Not Known if no notification has that id. Never transitions.

Kind: Operation

Pending For

The read-only query returning the Notification Id values of all Pending notifications addressed to a Recipient Reference (in the order Execution Contract Read 5 states; excludes terminals, Operation 20). Never transitions.

Kind: Operation

Notification Id

The opaque, immutable identity of a notification — host-allocated at the I/O seam (the injected id), produced by Create, never reused (Invariant 6). The recipient and payload are properties of the notification, not its identity.

Kind: Field Field of: the notification record Projection: notification_id

Recipient Reference

The opaque reference to the intended recipient. Set on Create, immutable. Equality is byte-exact (no normalization); Pending For filters on it.

Kind: Field Field of: the notification record Projection: recipient_ref

Payload

The opaque content of the notification. Set on Create, immutable, stored and returned unchanged — never parsed, validated, or interpreted by the atom.

Kind: Field Field of: the notification record Projection: payload

Creation Instant

The wall-time the notification was created, stamped from the injected clock at Create. Immutable (Invariant 1). The lower bound for any terminal timestamp (Invariant 8).

Kind: Field Field of: the notification record Projection: created_at

Status

The notification’s lifecycle state — Pending, Delivered, Failed, or Expired. Set to Pending on Create; transitions once to a terminal (State 1, Invariant 2).

Kind: Field Field of: the notification record Projection: status

Delivery Instant

The wall-time delivery was confirmed, stamped at Deliver. Present iff status is Delivered (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projection: delivered_at

Failure Instant

The wall-time the failure was recorded, stamped at Fail. Present iff status is Failed (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projection: failed_at

Lapse Instant

The wall-time the expiry was recorded, stamped at Expire. Present iff status is Expired (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projection: expired_at

Pending

The non-terminal state of a created notification whose delivery has not been confirmed, failed, or expired. May transition to exactly one terminal; Pending For returns only records in this state.

Kind: Member Member of: the notification status Role: Outcome

Delivered

The terminal state of a notification that reached the recipient (transport confirmed). Carries Delivery Instant; absorbing (Invariant 2).

Kind: Member Member of: the notification status Role: Outcome

Failed

The terminal state of a notification a composing pattern ended as failed, under the deployment’s declared fail-versus-expire policy (Operation 14, Capability requirement 8). Carries Failure Instant; absorbing.

Kind: Member Member of: the notification status Role: Outcome

Expired

The terminal state of a notification a composing pattern ended as expired, under the deployment’s declared fail-versus-expire policy (Operation 14, Operation 14b, Capability requirement 8). Carries Lapse Instant; absorbing.

Kind: Member Member of: the notification status Role: Outcome

Now

The current clock reading every writing action consumes — supplied at the atom’s seam, never read inside the transition and never a signature parameter. Its only use is the immutable stamps inside committed transitions (Creation Instant and the terminal stamp).

Kind: Parameter Parameter of: Create, Deliver, Fail and Expire Projection: now

Invalid Request

The refusal Create returns when a request field fails its rule — a blank Recipient Reference (Operation 4), a malformed Recipient Reference (Operation 31), or a recipient reference over the deployment’s cap (String 6). An empty Payload is not a failure: Operation 5 accepts it.

Kind: Member Member of: the Create rejection Role: Outcome Projection: invalid-request

Not Known

The refusal Deliver, Fail, or Expire returns when the Notification Id references no notification in the database (Operation 8) or is malformed (Operation 32). Also the Status Of outcome for an unknown id (Operation 18) or a malformed id (Operation 18b).

Kind: Member Member of: the action rejection Role: Outcome Projection: not-known

Not Pending

The refusal Deliver, Fail, or Expire returns when the target is not in Pending — i.e., already in a terminal state.

Kind: Member Member of: the action rejection Role: Outcome Projection: not-pending

Storage Failure

The refusal Create, Deliver, Fail or Expire returns when the database refuses the call’s write after its guards pass (Operation 7, Operation 15). The notification records stand as the call found them (Operation 16), and a caller reads it from Deliver as a notification still pending (Deliver persistence 1).

Kind: Member Member of: the action rejection Role: Outcome Projection: storage-failure

Standards references

Observer pattern (GoF — the Gang of Four, the four authors of Design Patterns) — Notification is the structured-natural-language realization of the notification object: the message delivered from subject to observer.
SMTP / RFC 5321 — SMTP (Simple Mail Transfer Protocol, defined in the Internet standard RFC (Request for Comments) 5321) email delivery as the canonical push transport. Two of the three terminal states map to an SMTP disposition: 2xx success (Delivered) and 5xx permanent failure (Failed); timeout without delivery (Expired) maps to none, since SMTP has no terminal disposition for it and the composing pattern owns the delivery window (Operation 14b).
HTTP (HyperText Transfer Protocol — the request/response protocol of the web) webhooks — POST-to-URL delivery model standard in web systems. Deliver records a 2xx response; Fail records a 4xx/5xx or connection failure.
W3C (World Wide Web Consortium — the web standards body) Activity Streams 2.0 — semantic vocabulary for describing social and messaging events. Notification payloads in web deployments often conform to Activity Streams objects.
Apple Push Notification Service / Firebase Cloud Messaging — platform push notification services where Deliver corresponds to accepted delivery and Fail corresponds to a rejected or unregistered token.
Daniel Jackson, The Essence of Software — freestanding-atom posture; Payload as an opaque reference whose semantics are defined by the composing system.
Eiffel’s design-by-contract — preconditions on Deliver, Fail, and Expire; named rejection reasons.

Status

grounded on Final Critique 11 — 2026-11-05 at 917cc95 — see the Ledger.

Ledger

status: grounded on Final Critique 11 — 2026-11-05 at 917cc95
formal: verified — notification.als + 1 twin, 2026-06-03
last gate: 2026-11-05 — Final Critique 11, a full round, frozen at 917cc95 — foundational count 0, clean, one sample; 2026-11-05 — Final Critique 10, a delta round, frozen at 82d4603 — foundational count 1, cured, not clean, no sample; 2026-11-05 — Final Critique 9, a delta round, frozen at 29128b6 — foundational count 1, cured, not clean, no sample; 2026-11-04 — Final Critique 8, a delta round, frozen at 075c6e4 — foundational count 1, cured, not clean, no sample; 2026-11-03 — Final Critique 7 — foundational count 2, not clean, no sample

open:
- 2026-10-21-b · refining · Examples (Shared Todo) · the three outcomes of notif_77 (delivered, failed, expired) share one notification, and only each paragraph's condition says they are alternatives, so a sequence test compiled from the walkthrough can read them as one sequence that breaks Invariant 2.3 → name each outcome an alternative, or give each its own notification
- 2026-10-21-f · refining · Operations (signature block) · the success arm ok and the answer arm notification_ids resolve to no declaration (GRACE-lang Closed vocabulary 4, 27), the corpus's form on sixteen and seven specifications → declare each, or settle in the grammar whether an arm owes a term entry
- 2026-10-21-g · refining · Deliver persistence 4 · a high-assurance deployment is declared nowhere, and the alert names no receiver → declare the class and the receiver, or say whose they are
- 2026-11-05-a · refining · Bulk expiry 1, Bulk expiry 2 · the two rules bind every composing pattern as written, where Non-goal 4 and Payload retention 4 carry the conditioned form (IF a composing pattern expires in bulk THEN …) → condition both on a composing pattern that expires in bulk, once the corpus settles whether a bulk expiry is a composing pattern's obligation or a deployment's

Decisions

Directional changes only — the turns a future reader must know the pattern took, and why. Everything smaller lives in the commit that made it: git log -- atoms/notification.md; the migration that got it here is in its history.

2026-11-02 — The string cap has a default. Chose: the string cap stated as 256 Unicode code points where a deployment declares none, Capability requirement 5 turned to declare, citing Execution Contract Input 2. Over: a bound the deployment must supply, or silence. Because: the maintainer ruled on 2026-11-01 that what the host must bound takes one posture, a corpus default a deployment may override; the one string input the cap bounds is the recipient reference, an opaque reference, and 256 code points holds an email address (254) with room to spare; the payload stays outside the cap, as the page left it, and String 6 and Capability requirement 6 stand.
2026-10-20 — The store’s guarantees cited, not restated. Chose: the notification store supplied under Execution Contract Store 1 through 4 (Capability requirement 4), and the four rules that restated them tombstoned to their owner — Terminal atomicity 1, a terminal transition changing status and the terminal stamp together, to Store 1; Terminal atomicity 2 and 3, no crash inside a terminal transition leaving a terminal status without its stamp or a stamp on a pending notification, to Store 1 and Store 3; Terminal atomicity 4, two terminal transitions on one notification id serialized, to Store 2; rules 130 to 127. Over: the atom restating, for its own store, what every deployment’s store guarantees. Because: the maintainer ruled 2026-10-12 that the corpus takes a store’s specification, never the store, and execution-contract.md writes it once as the Store contract. A refused call leaving the notification as the call found it stays the atom’s own (Operation 16), as do the caller’s reading of a refused deliver (Deliver persistence 1 through 4), the payload kept for the store’s life and a composed purge leaving every stored field as written (Payload retention 1 through 5), the recorded fields and a landed stamp that never change (Invariant 1.1, Invariant 1.2) and the atom’s durability (State 10, Invariant 9.1 through 9.3). Pending at an instant is read from the creation instant and terminal stamp each notification carries, and Pending For answers unordered, so the atom cites neither History 1 nor Order 1. What the atom does for its domain is unchanged.
2026-10-21 — The string cap bounds the recipient reference, and the deployment supplies it; a failed read answers on every action, each writing shape’s refusals in one stated order; the wiring declaration is an external check. Chose: String 6’s cap on the recipient reference alone, the payload left unmeasured as Operation 6 and Non-goal 10 say (a payload too large to keep is the database’s refusal, Operation 7), and Capability requirement 5 obliging the deployment to supply the cap; state-unavailable on all six actions where the read of the notification records fails, the Execution Contract’s Step 1 failure (Operation 27, Term database read), Create’s refusals and a terminal transition’s each evaluated in one order with the read first (Operation 28, Operation 29), and the reads’ answer rules held to an answered read (Operation 17 through 19, Invariant 9.3); Check 6.1 deleted to External check 5, the auditor reading which composing patterns a deployment wired in from the deployment’s own declaration. Over: a cap that reached a payload the atom may neither read nor validate, as Final Critique 4’s String input policy had it reach both string inputs; a cap no rule obliged anyone to supply; six actions with no answer for a read that fails; and a conformance check no notification record can answer. Because: Final Critique 5 found each a divergence between conforming builds, two rules no build can both obey, or a check a conforming deployment fails, and the corpus held each cure: the page’s own payload rules, which say four times that the atom never reads a payload; the requirement form Credential, Party Identity and Medication Order give a length bound; the failed-read form Actor Identity, Approval Step, Capability and Duplicate Prevention carry; and the external check to which six atoms moved the same check. What each action does on a call it admits is unchanged, save that a payload is no longer measured against the cap.
2026-10-21 — A failed read answers as the Execution Contract says. Chose: the failed read cited from the Execution Contract (Capability requirement 4, Execution Contract Read 1 through 3) and the two rules that restated it deleted to it: the atom-wide state-unavailable (Operation 27) to Read 1, and the create refusal order (Operation 28), whose rules after the read both answer invalid-request, to Read 1; the read’s condition off the read answers it held to an answered read (Operation 17 through 19, Invariant 9.3), the read off the terminal refusal order, Term database read deleted, and state-unavailable off every signature and the case table; rules 131 to 129. Over: the page stating for itself what every action answers when the notification records cannot be read. Because: the maintainer ruled on 2026-10-21 that the Execution Contract states the failed read once; this page’s fifth Final Critique had made one of the cures the contract’s Read family is written from. What each action answers on an answered read is unchanged, and Invariant 9, which Notification Fanout cites, holds on every answered read as it did.
2026-10-21 — Which refusal answers is the Execution Contract’s. Chose: each terminal transition’s refuses line kept as the page wrote it, already in the order the terminal refusal order gave — not-known, not-pending, then storage-failure, which answers only at the write — and the order cited from the Execution Contract (Capability requirement 4, Execution Contract Refusal 1); Operation 29, which evaluated the terminal refusal order, deleted to Refusal 1, and Term terminal refusal order deleted with it; rules 129 to 128. Over: the page stating for itself which of a terminal transition’s refusals answers when both apply. Because: the maintainer ruled on 2026-10-21 that the Execution Contract states once that the refusal listed first on an action’s refuses line answers; this page’s fifth Final Critique had made the cure one specification at a time. What each action answers on every call is unchanged.
2026-10-22 — The wiring is read outside the records, as the Execution Contract says. Chose: External check 5, the auditor reading which composing patterns a deployment wired in from the deployment’s own declaration, deleted to Execution Contract Conformance 9, with Check 6.1’s tombstone, which named it, now naming the contract, the checks NOTE’s sentence restating it removed, and the label cited on Capability requirement 4; rules 128 to 127. Over: the page stating for itself that the wiring is an external check. Because: the maintainer ruled on 2026-10-22 that five repeated cures are each stated once, the wiring declaration among them; this page’s fifth Final Critique had made the cure one specification at a time. What each action does and answers is unchanged, and Invariant 9, which Notification Fanout cites, stands as it was.

NOTE: End of Notification.