Temporal obligations

A MONITOR states bounded requirements over correlated events: when a trigger occurs, a response must follow within a horizon, or a forbidden event must not. Evaluating a finite trace distinguishes a disproved obligation from insufficient evidence.

repair_promise = MONITOR ON events AS event
  KEY event.job_id
  TIME event.occurred_at
  MATCH ALL

  WHEN event.kind = :accepted AS acceptance
  EXPECT event.kind = :completed AND event.job_id = acceptance.job_id WITHIN 8min
END

inspection = repair_promise.REPORT(trace, {
  as_of: 16min,
  coverage: {through: 16min, basis: :caller_asserted}
})

MONITOR repair_promise ON events AS event … END is the equivalent declaration spelling. ON names a typed input port, not a subscription; the alias exposes each event's payload. The definition binds EVALUATE and REPORT members. Reading or importing it attaches nothing and reads no clock.

Clauses

KEY and TIME are pure expressions over one event. Keys are immutable scalar values or fixed-shape records of scalar keys, with type-sensitive equality. A composite key such as {tenant: event.tenant, job: event.job} keeps tenants separate. Times are all numbers or all durations (4min); mixing domains is an error. MATCH ALL offers an event to every eligible obligation; MATCH OLDEST lets it discharge only the oldest open obligation of its clause and key.

A monitor has one unnamed clause or several named OBLIGATION label … END blocks, each with one WHEN trigger [AS alias] and one goal:

Goal	Meaning over the inclusive interval [trigger, trigger + h]
EXPECT predicate WITHIN h	At least one matching event
AVOID predicate FOR h	No matching event (requires MATCH ALL)
EXPECT AT LEAST n MATCHING predicate WITHIN h	At least n matches
EXPECT AT MOST n MATCHING predicate WITHIN h	At most n matches; closure is required
EXPECT EXACTLY n MATCHING predicate WITHIN h	Exactly n matches; closure is required
REQUIRE PRIOR predicate [AS alias] WITHIN h	A qualifying witness within the bounded earlier interval
EXPECT SEQUENCE WITHIN h … END	Ordered STEP predicates with bounded alternative prefixes

The goal predicate sees the candidate as the event alias and the frozen trigger as its alias. A trigger never satisfies itself; other events at the same instant may. Horizons may use parameters and the trigger. Predicates must produce booleans; an error or a non-boolean fails the evaluation (MONITOR_PREDICATE_ERROR, MONITOR_PREDICATE_TYPE) rather than becoming false.

Finite evaluation

EVALUATE(trace, options) and REPORT(trace, options) take a List of event records or a complete immutable Frame snapshot, and an options record with optional from, as_of, parameters (required when the monitor declares parameters) and coverage with an optional inclusive from, exclusive through, basis and origin. Omitting coverage.from asserts a prefix with no lower boundary; an explicit boundary does not imply earlier history. Reversed coverage intervals are errors. Triggers are discovered in [from, as_of]; events after as_of provide no evidence. EVALUATE returns OK(evaluation) or ERR(problem). REPORT returns a plain grid.monitor.report.v1 record whose outcome is exactly that Result from the same execution. An unsuccessful report has status: :evaluation_error; it is not a committed business verdict.

Each obligation row carries its clause, key, trigger ordinal and time, deadline, lower bound, status, final, witness, stable witnesses, observedCount and reason:

Status	Meaning
pending	The deadline is after as_of
satisfied	The goal is established over covered evidence
violated	The goal is disproved over covered evidence
cancelled	A correlated cancellation won under the explicit tie rule
indeterminate	Required coverage or progress does not establish a verdict

A missed response becomes a violation only when coverage.through is later than the inclusive deadline; otherwise the row is indeterminate, because absence of an event is not evidence without declared coverage. A completion exactly at the deadline satisfies. coverage_complete is true when the declared coverage covers and seals the whole scope and no row is indeterminate. Absence-based verdicts require coverage starting at or before the trigger. OLDEST also needs activation history: a missing prefix may change which obligation owns an observed response, so a witness alone cannot settle it.

Rows are ordered by clause, canonical key, trigger time, explicit order and stable event identity. Reports add evaluation counts (events, predicate calls, clauses, candidateVisits and workUnits). Completed and expired obligations leave the active index. Candidate visits, including skipped self-candidates, callable invocations, retained-state traversal and result construction share a 20-million-unit work ceiling; exceeding it returns MONITOR_BUDGET.

Distinct counts, prior evidence and sequences

DISTINCT expression counts unique keys rather than repeated acknowledgments. BETWEEN lower AND upper replaces a goal's zero-based interval; both boundaries are inclusive. Counts and horizons may depend on the frozen trigger. Reaching a minimum can establish it before closure; an exact or maximum count must wait until the interval is sealed.

REQUIRE PRIOR predicate AS approval WITHIN h may add UNLESS predicate, which can refer to the candidate approval and the trigger. Revoking the newest candidate does not hide an older still-valid approval. The lookback must be covered; missing history yields indeterminate evidence.

Sequences use named steps, optional captures and per-step deadlines:

EXPECT SEQUENCE WITHIN 10min
  STEP accept WHEN event.kind = :accepted AS acceptance
  STEP ship WHEN event.parent = acceptance.id WITHIN 5min
END

Alternative prefixes remain available until they expire or complete. A later step cannot reuse the same event occurrence. ORDER expression disambiguates same-time ordering within a key; duplicate order positions are errors. A bare timestamp does not establish that one simultaneous event preceded another.

CANCEL WHEN predicate adds business cancellation to a future obligation. Choose TIE CANCEL, TIE DECIDE or TIE ERROR explicitly when cancellation and decision share a timestamp. All peers at that timestamp are considered; arrival iteration order cannot decide the tie. Cancellation does not apply to an already decided prior-evidence requirement.

An optional EVENT Type checks the payload before any projection or predicate. All expressions retain ordinary Grid name binding, precedence and type rules. See repair promises for distinct acknowledgments, cancellation and a genuinely late completion.

Envelopes, partitions and clocks

For replayable evidence, select the envelope fields explicitly: id, source, partition, cursor, payload and time. Identical repeated identities are idempotent. Reusing an identity with different content or a cursor for a different event is an error. Raw business column names are never inferred to be these fields.

Declare partition membership with {source, partition, epoch} records. Progress supplies the same identity, a covered from, and either an exclusive watermark or inclusive complete_through. Every partition must seal the relevant time before global absence is established. Gaps remain explicit; observing a later event does not prove earlier coverage. Events behind a published seal and regressing progress are refused.

TIME PROCESSING uses recorded ingress receipt timestamps under an explicitly selected processing-clock adapter. It never reads the wall clock during a formula call. Replay must preserve those timestamps and the original receipt and progress-control order. Native millisecond adapters require exact safe integer times; ordinary duration inputs remain duration values.

Explicit live attachment

A live application attaches through the existing Host Stream owner, selecting the compiled definition, parameters, source membership/clock, activation boundary, horizon/lookback limits and bounded receipt/state sizes. A provider must atomically commit consumed receipts, the checkpoint and its durable local output batch. Attachment fails if that guarantee is unavailable. Merely reading a monitor or its result does not subscribe, poll, start a worker or publish an external effect.

The continuation retains sealed counts, distinct sets, sequence alternatives and captures. It replays only unsealed events for provisional inspection; those projections do not consume committed state. Backfill is an explicit bounded snapshot with provenance and original ingress timestamps. Its progress controls establish coverage, and source identities reconcile the handoff to live receipts. Changed backfill or definition/parameter/source contracts require a new attachment identity.

Reopening validates the checkpoint and retained outcome. Detach checkpoints unresolved rows; it does not turn them into cancellations or successes. Receipt failure or cancellation leaves the receipt available and the committed revision unchanged. A source-contract contradiction persists a coverage fault without acknowledging the bad receipt or rewriting final verdicts. Inspection then reports incomplete coverage and refuses complete-result publication.

Inspection reads committed state without advancing receipts. Explicit Frame publication uses the existing model Frame owner and preserves typed statuses, Options and witness Lists. Notifications and enforcement are separate rule or workflow effects. A local output transaction makes no exactly-once promise about email or remote services.

Bounds and result carriers

The finite evaluator accepts explicit event Lists and complete immutable Frames. Frame input requires an explicit envelope adapter. A complete inline Frame carries its columns; external handles require the scoped model Frame provider. Typed payloads and stable identities have the same meaning as in a List. Incomplete extents, inconsistent row counts and foreign external Frames are refused. The evaluator returns a complete immutable obligations Frame with its thirteen declared columns, including zero-row results. Status symbols, Options and witness Lists keep their native types. Constructing or reading that result does not publish files or start a Job. Explicit queries and Host publication use the existing Frame owners. The implementation record distinguishes functional verification from the separately deferred performance measurements.

The selected live profile retains at most the admitted event identity limit (up to 200,000) and 100,000 obligations. Payloads can retire after a sealed frontier and the required lookback, while identity and output metadata remain bounded. Exhaustion fails closed; there is no silent expiry that makes an old duplicate look new or turns missing history into complete evidence. The local output is an as-of snapshot, not an unbounded audit log. An explicit artifact/Frame owner must retain any requested historical snapshots.

The initial replacement policy is explicit replay into a new binding. Stop and checkpoint the old binding with set_stopped(true), retaining its unresolved rows, then call attach_monitor_stream_with_backfill with a new consumer/region identity and output subscription. Supply the new definition/parameters and the retained source envelopes, their original source epochs and receipt times, and explicit coverage controls. A changed contract cannot reuse the old checkpoint. Failed replay leaves the old binding stopped and acknowledges no live input; retrying the same successfully retained history reuses the new checkpoint. An operator may explicitly resume the old binding as a separate operation. This protocol does not claim an atomic cross-binding switch or automatically cancel old obligations.

General temporal logic, unbounded repetition, calendar deadlines, continuous signal proofs and provisional/corrective external effects are outside this profile.