Conseqa Operation Requirements: Serialization, Ordering, Idempotency, and Recoverability

Operation requirements are proof obligations. Declaring one does not assert that the operation already satisfies it. The verifier must prove it from the declared facts and architecture.

​

Serialization

A serialization requirement keyed by a ValueRef means:

Invocations with the same logical key must not execute concurrently.

Different keys may execute concurrently unless constrained elsewhere. Serialization establishes mutual exclusion and non-overlap. It does not establish which same-key invocation should come first. V1 accepts four discharge routes. In every non-vacuous route, the target pool must declare member_concurrency = bounded(1) and the routing domain must have a single owning member.

​

Vacuous population

The key’s message-driven input admits no message schemas, so the constrained population is empty by declaration. This is the only l0_only route.

​

Request-routed

A Router serves the key’s request boundary. Every component of its semantic routing key carries the same logical value as the requirement key. Its MemberAssignment gives that domain one active owning member (including through safe ownership transfer), and the target pool declares member_concurrency = bounded(1).

​

Subscription-routed

The same argument on the delivery side, with key: grouping_key naming the effective grouping domain and the requirement key established to carry the grouping key for every admitted schema.

​

Outbox-routed

The same argument over an outbox input’s keyed partitioning. The dispatch’s MemberAssignment gives each partition one active owning member, the pool is serial, and the dispatch declares no batching stage. A declared batching stage stops the serialization route outright: batch-internal overlap is intentionally unmodeled.

​

Ordering

An ordering requirement keyed by a ValueRef means:

Same-key invocations for which a meaningful logical precedence exists must preserve that precedence through the operation’s semantically relevant execution.

A proof must establish both where the relevant precedence comes from and that the execution mechanism preserves it. Arbitrarily serializing concurrent inputs can satisfy a serialization requirement but cannot invent a semantic precedence required by an ordering proof.

​

Precedence sources

V1 recognizes two precedence sources:

1. Transport ordering (within_group or global) for a subscription-triggered key.
2. Outbox ordering (partition or global) for an outbox-triggered key.

A request input has no precedence source at all, so a request-routed boundary proves serialization but not ordering.

​

Mechanism

The mechanism is the serialization argument plus a precedence: the requirement key is established to be the effective grouping key for every admitted schema, key: grouping_key routes by that same domain, MemberAssignment gives it one active owning member, and member_concurrency = bounded(1) stops a later invocation from overtaking an earlier one. Dispatch preserves precedence and never creates it, so dispatch alone can never supply ordering.

​

Batching and ordering

A declared batching stage is judged explicitly. ordering: preserved lets the established precedence pass through the stage. ordering: unspecified stops the proof, because the stage then provides no evidence the order survives execution. Order preservation is an ordering fact only: it is never read as a no-overlap guarantee, which is why serialization refuses batching outright while ordering accepts preserved.

​

Idempotency

An idempotency requirement identifies a logical invocation by a composite IdempotencyKey. It means:

Repeated attempts representing the same logical invocation must not cause externally distinguishable duplicate logical work beyond what the declared idempotency contract permits.

V1 discharges the requirement over each admitted path under the governing key’s population. Three legs must hold on every admitted path:

​

State leg

Every transaction step must be retry-safe: a keyed commit over a stable key, or naturally replayable.

​

Effect leg

Every effect-executing step must be duplicate-safe. A request is safe only when its target collapses duplicate invocations. A publication is safe only when every modeled consumer collapses duplicate deliveries. An outbox write is safe when its containing transaction suppresses a second commit, or every modeled consumer collapses duplicate deliveries. An outbox boundary does not terminate the causal effect graph: the cascade continues through every outbox input admitting the written schema.

​

Control leg

Every decision on the path must replay: the matched result replay-stable, or the branch condition deterministic over replay-stable roots, so every attempt in the class traverses the same path. Mutually dependent verdicts are computed as a greatest fixpoint: a cycle of requirements that each collapse the others’ duplicates is proven and marked coinductive.

​

Result replay

The result member of an idempotency requirement asks a further question:

Repeated admitted attempts in the same logical idempotency class that return a request result must return the same result variant and a replay-equivalent payload.

V1 discharges this, for each admitted path ending at a return for the triggering input, when:

1. every decision on the path replays, and
2. the terminal’s derivation is replay-deterministic in the context at the terminal.

Premise 2 may name other operations’ verdicts, since a bound request result is stable only when the target proves its result replay-consistent for the targeted input. These checks are also computed as a greatest fixpoint.

​

Recoverability

A recoverability requirement keyed by an IdempotencyKey means:

The logical invocation identified by that key must reach a valid terminal of the operation program after any modeled interruption.

Recoverability is a progress obligation. Idempotency is a safety obligation. They are deliberately separate because neither implies the other.

​

resumable

An interrupted attempt must be able to resume and drive the program to a terminal. V1 discharges this by same-path continuation: for every admitted path, re-driving that same path from its first step must reach the path’s terminal. A decision is never an obstacle to progress.

​

guaranteed

The architecture must guarantee that the logical invocation is re-driven until the program reaches a terminal. This additionally requires a modeled retry driver:

• delivery: at_least_once on the triggering subscription’s runtime or on the triggering outbox input’s runtime (runtime-dependent proof)
• an inbound RequestEffect whose retry is may_repeat (L0-only proof)

A guaranteed recoverability proof for an operation that declares no idempotency requirement carries a warning, because the driver makes retries expected and nothing declares them safe.