Conseqa DSL Effects: Publication, Request, External

Effects are how an operation interacts with the world outside its own transaction state. They cover publishing messages to topics, calling other operations, and invoking external systems. Effect contracts owned by an operation are declared inline at the exact program or transaction step that executes or establishes them. There is no operation-level effect registry; the execution site is the source of truth for both the contract and the concrete values that instance carries. State-machine transitions are the one place effect contracts live outside a specific execution site: transition side-effect contracts are shared model-level declarations owned by the state machine (see State Machines).

Effect contracts and effect instances

An effect declaration is a contract. It describes the kind of work, the destination, the schema, the retry or idempotency guarantee, and any key propagation. It does not by itself say what specific values a particular instance carries, those are fixed at each execution or establishment site:

an execute_effect program step declares the effect contract inline and runs the effect directly, with a values derivation;
an establish_effect_intent transaction step declares the effect contract inline, constructs one concrete effect instance from values, and captures it as a durable intent artifact bound by name;
an execute_effect_intent program step runs a previously established intent by binding name, the values were fixed at establishment and are not recomputed.

Every operation-owned inline effect site carries an effect_id. That ID identifies the inline effect occurrence itself and is what ValueSource::Effect resolves to in idempotency-key propagation. effect_id values must be unique across all inline effect sites within a single operation.

Publication effect

A publication effect sends a message carrying one schema to one topic. Publications have no synchronous result: you cannot bind a result from executing a publication.

# Directly executed publication
- kind: execute_effect
  effect_id: effect.notify.publish_dropped
  effect:
    kind: publication
    topic: topic.notifications
    schema: schema.NotificationDropped
    idempotency_key_propagation: []
  values:
    kind: deterministic
    from:
      - source: input:input.notify.request
        path: notification_id

# Publication captured as an intent inside a transaction
- kind: establish_effect_intent
  bind: intent.create_order.publish_created
  effect_id: effect.create_order.publish_created
  effect:
    kind: publication
    topic: topic.order_events
    schema: schema.OrderCreated
    idempotency_key_propagation:
      - source:
          components:
            - source: input:input.create_order.request
              path: idempotency_key
        target:
          components:
            - source: effect:effect.create_order.publish_created
              path: event_id
  values:
    kind: deterministic
    from:
      - source: input:input.create_order.request
        path: order_id
      - source: input:input.create_order.request
        path: idempotency_key

string

required

Must be publication.

required

The topic to publish to. Must be declared in the model’s topics map, and the schema must appear in topic.messages.

required

The schema of the published message.

list[IdempotencyKeyPropagation]

required

Declares that certain values in the published payload carry the same logical idempotency identity as upstream values. This is a lineage assertion, it does not deduplicate publications. See Idempotency key propagation.

When a duplicate publication is safe

For an upstream idempotency requirement, a repeated publication is safe only when two conditions both hold:

The topic declares a keyed message_identity mapping the published schema, and the published instance is class-fixed (replay-deterministic for a direct execution, or available by route A or B for an intent). Every attempt then publishes the same logical message.
Every modeled consumer of that message collapses duplicate deliveries, either through a proven idempotency requirement keyed from that subscription, or because the subscription declares delivery: at_most_once.

A publication declaration alone does not imply exactly-once delivery, atomic commit, deduplication, or that the effect runs at all.

Request effect

A request effect invokes a specific request input of another operation. It inherits the Result<Ok, Err> contract declared on the target input, you do not redeclare the result schema on the effect.

- kind: execute_effect
  effect_id: effect.notify.send_confirmation
  effect:
    kind: request
    target:
      operation: operation.email_service
      input: input.email_service.send
    schema: schema.SendEmailRequest
    retry: may_repeat
    idempotency_key_propagation:
      - source:
          components:
            - source: input:input.create_order.request
              path: idempotency_key
        target:
          components:
            - source: effect:effect.notify.send_confirmation
              path: request_id
  values:
    kind: deterministic
    from:
      - source: input:input.create_order.request
        path: order_id
  bind: result.notify.send_confirmation

string

required

Must be request.

object

required

Identifies the destination operation and input.

operation — the ID of the target operation
input — the ID of the request input within that operation

required

The schema of the outbound request payload. Must match the target input’s declared schema.

string

required

Declares whether the requesting boundary may issue repeated attempts for the same logical request.

never — the mechanism does not intentionally repeat the request. This is a sender-side fact only; it does not guarantee exactly-once delivery across all failure modes.
may_repeat — the logical request may be attempted more than once. Downstream duplicate invocation must be expected.
unspecified — no retry fact is declared. The verifier treats this as unknown.

list[IdempotencyKeyPropagation]

required

Links outbound request key fields to upstream logical identity. See Idempotency key propagation.

Inherited result contract

A request effect’s synchronous result is exactly the Result<Ok, Err> declared on the targeted input. Bind it at the execution site with bind:

- kind: execute_effect
  effect_id: effect.notify.send_confirmation
  effect:
    kind: request
    target:
      operation: operation.email_service
      input: input.email_service.send
    schema: schema.SendEmailRequest
    retry: may_repeat
    idempotency_key_propagation: []
  values:
    kind: deterministic
    from:
      - source: input:input.create_order.request
        path: order_id
  bind: result.notify.send_confirmation   # binds the result for match_result

When a duplicate request is safe

A duplicate request invocation is safe when the executed instance is class-fixed, the effect’s schema matches the target input’s schema, and the target operation declares a proven idempotency requirement keyed from that input. Payload-equal duplicates then fall into one class of that requirement, which collapses them to the work of a single logical invocation.

External effect

An external effect marks a boundary Conseqa cannot inspect. Because the verifier cannot analyze the external implementation, you must explicitly declare its idempotency behavior and, if applicable, its synchronous result.

- kind: execute_effect
  effect_id: effect.charge_payment.card
  effect:
    kind: external
    name: payment-provider.charge
    idempotency:
      kind: not_deduplicated
    result:
      ok: schema.ChargeAccepted
      err:
        schema: schema.ChargeDeclined
        disposition: terminal
  values:
    kind: unspecified
  bind: result.charge_payment.card

- kind: execute_effect
  effect_id: effect.notify_published.push
  effect:
    kind: external
    name: push-gateway.notify
    idempotency:
      kind: deduplicated_by
      key:
        components:
          - source: input:input.notify_published.published
            path: event_id
    result: null
  values:
    kind: deterministic
    from:
      - source: input:input.notify_published.published
        path: event_id

string

required

Must be external.

string

required

A descriptive label for the external system. Used in diagnostics and reports; has no proof semantics.

object

required

Declares the external boundary’s deduplication guarantee. One of three forms:

kind: unspecified — no deduplication fact is available. The verifier treats duplicate executions as potentially unsafe.
kind: not_deduplicated — repeated execution is explicitly not deduplicated. A retry path reaching this effect is potentially unsafe for an upstream idempotency requirement.
kind: deduplicated_by with a key — the external boundary guarantees deduplication for executions sharing the declared key. A duplicate execution is safe when every component of the key is replay-stable relative to the governing key.

object | null

required

The synchronous result the boundary returns, or null if no result is modeled.When present, declare:

ok — the ID of the Ok schema
err.schema — the ID of the Err schema
err.disposition — one of terminal, retryable, or unspecified

For a result-bearing effect with deduplicated_by, equal evaluated keys fix the terminal logical result: once the first terminal Ok or terminal Err is observed, every subsequent same-key execution returns the same variant and a replay-equivalent payload. A retryable Err does not establish a terminal result.

`ErrorDisposition` values

Value	Meaning
`terminal`	Observing this `Err` terminally resolves the logical interaction. The verifier can use it as a stable root.
`retryable`	This `Err` ends the current attempt but does not terminally resolve the interaction; another attempt is semantically admitted. The verifier cannot use it as a stable root.
`unspecified`	No terminality fact is declared. The verifier treats the observation as unknown.

A bare schema ID in err is shorthand for disposition: unspecified.

Effect intents

An effect intent is a durable transaction artifact that captures a specific effect instance for later execution. The intent pattern enables at-least-once execution across failures: the effect contract, its concrete values, and the resulting intent binding are all declared at the establish_effect_intent transaction step, so the captured instance commits atomically with application state and is recovered from that commit after a crash.

# Inside a transaction's steps: capture the intent
- kind: establish_effect_intent
  bind: intent.create_order.publish_created
  effect_id: effect.create_order.publish_created
  effect:
    kind: publication
    topic: topic.order_events
    schema: schema.OrderCreated
    idempotency_key_propagation: []
  values:
    kind: deterministic
    from:
      - source: input:input.create_order.request
        path: order_id
      - source: input:input.create_order.request
        path: idempotency_key

# Later in the operation's program: execute the captured instance
- kind: execute_effect_intent
  intent: intent.create_order.publish_created

required

The operation-local intent binding this transaction step establishes. Later program steps refer to this exact name in execute_effect_intent.

required

Stable identifier for this inline effect site. ValueSource::Effect(effect_id) (used in idempotency-key propagation and value lineage) resolves to this site.

Effect

required

The inline effect contract this intent captures. May be a publication or request; external effects with side effects that must be captured atomically follow the same shape.

Derivation

required

Provenance of the concrete effect instance captured by this intent. The values are fixed at establishment.

Establishing an intent atomically declares the effect contract, constructs one concrete instance from values, and establishes that captured instance as the bound artifact. execute_effect_intent runs the exact captured instance and does not recompute the values.

An intent declaration does not imply an automatic background executor. The intent executes only when a program step explicitly runs it via execute_effect_intent. Retry availability depends on whether the establishing transaction uses natural replay (route A) or an explicit deduplicated_by commit (route B).

Reconstructing or recovering the same intent does not prove that repeating the underlying external effect is safe. A crash after an external effect succeeds but before its completion is durably known may lead to another effect attempt, the effect’s own idempotency guarantee handles that uncertainty.

Transition-owned intents

State-machine transitions declare their own side-effect contracts. When a transaction applies a transition, the transition step’s effect_intents map binds each of the transition’s side effects into an operation-local intent artifact:

- kind: transition
  machine: machine.order_lifecycle
  transition: transition.order.mark_paid
  subject: ...
  effect_intents:
    effect.order.paid:
      bind: intent.apply_payment.order_paid
      values:
        kind: deterministic
        from:
          - source: input:input.apply_payment.captured
            path: order_id

The map key is the state-machine transition side-effect ID, coverage must be exact. Each entry supplies exactly one derivation and one intent binding. Later program steps execute the intent by binding name via execute_effect_intent.

Idempotency key propagation

idempotency_key_propagation on a publication or request effect declares that certain values in the outbound payload carry the same logical idempotency identity as upstream values. It is a lineage assertion that lets the verifier trace the same logical key across effect boundaries.

idempotency_key_propagation:
  - source:
      components:
        - source: input:input.reserve_inventory.created
          path: event_id
    target:
      components:
        - source: effect:effect.reserve_inventory.publish_reserved
          path: event_id

The source components identify the upstream key fields; the target components identify the corresponding fields in the outbound payload. The effect:<effect_id> reference resolves to the inline effect site that carries the outbound payload. Propagation does not deduplicate anything, it tells the verifier that a consumer observing the target fields is observing the same logical key as the producer’s source fields.

Propagation plays no role in the publication duplicate-safety discharge. A class-fixed publication instance already makes every duplicate payload-equal, so a consumer’s key evaluates the same across all duplicates regardless of whether propagation was declared.

Result bindings on effect execution

Both execute_effect and execute_effect_intent accept an optional bind field naming the effect result observation:

- kind: execute_effect
  effect_id: effect.charge_payment.card
  effect: ...
  values: ...
  bind: result.charge_payment.card

- kind: execute_effect_intent
  intent: intent.transcode_video.completed
  bind: result.transcode_video.completed

The binding is valid only when the underlying effect contract is result-bearing (request effects, and external effects with a declared result). Publications have no result and must not declare bind. Effect result bindings are attempt-local observations, not transaction artifacts.

Outbox write effect

An OutboxWriteEffect admits one typed logical message to a data-model outbox. It is the only mechanism that writes to an outbox, and it is legal exclusively inside a write_outbox transaction step. The write is atomic with the containing transaction commit: T commits ⇒ mutations commit AND message admitted; T aborts ⇒ neither.

write_outbox step inside a transaction

- kind: transaction
  id: tx.place_order
  data_model: data.orders
  isolation: read_committed
  idempotency:
    kind: deduplicated_by
    key:
      components:
        - source: input:input.place_order.request
          path: idempotency_key
  steps:
    - kind: insert
      object: object.order
      values:
        kind: deterministic
        from:
          - source: input:input.place_order.request
            path: order_id
    - kind: write_outbox
      effect_id: effect.place_order.emit_placed
      effect:
        outbox: outbox.order_events
        schema: schema.OrderPlaced
        idempotency_key_propagation:
          - source:
              components:
                - source: input:input.place_order.request
                  path: idempotency_key
            target:
              components:
                - source: effect:effect.place_order.emit_placed
                  path: event_id
      values:
        kind: deterministic
        from:
          - source: input:input.place_order.request
            path: order_id
          - source: input:input.place_order.request
            path: submitted_at

Fields on the contract:

outbox — the target outbox id declared under data_models.<id>.outboxes.
schema — the admitted message schema. It must be listed in the outbox’s messages.
idempotency_key_propagation — same shape as for other effects.

The step carries the effect_id and the values derivation; there is no separate execute_effect for an outbox write. Because the write commits atomically with the transaction, an OutboxWriteEffect has no synchronous result, no async form, and cannot be bound. It is also never a transition side effect (transition may only establish request/publication/external intents).

An outbox write is rejected by every other execution site: execute_effect, execute_effect_async, execute_effect_intent, execute_effect_intent_async, and establish_effect_intent. Attempts to run an outbox write outside a write_outbox step are validation errors.

Producer-suppressed versus consumer-collapsed duplicate discharge

Duplicate discharge for outbox writes has two routes:

Producer-suppressed — the containing transaction declares deduplicated_by { key }, so a repeated commit under the same key is suppressed and no duplicate message is admitted at all.
Message- or consumer-routed — every modeled consumer of the outbox collapses duplicate deliveries (via its own idempotency requirement).

Either route discharges the effect leg of the operation’s idempotency requirement for that write. Both are computed as part of the greatest-fixpoint idempotency analysis (see Requirements).

Summary of effect kinds

Kind	Has synchronous result?	Idempotency declared how?
`publication`	No, cannot bind a result	Via topic `message_identity` plus consumer requirements
`request`	Yes, inherits from target input	Via target operation’s idempotency requirement
`external`	Optional (`result:` or `null`)	Explicitly: `unspecified`, `not_deduplicated`, or `deduplicated_by`
`outbox_write`	No, atomic with transaction	Producer-suppressed (`DeduplicatedBy`) or consumer-collapsed

Program Control

How to execute effects using execute_effect and execute_effect_intent steps

Value References

How to declare the values derivation for effect execution sites

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Conseqa DSL Effects: Publication, Request, External

Effect contracts and effect instances

Publication effect

When a duplicate publication is safe

Request effect

Inherited result contract

When a duplicate request is safe

External effect

`ErrorDisposition` values

Effect intents

Transition-owned intents

Idempotency key propagation

Result bindings on effect execution

Outbox write effect

Producer-suppressed versus consumer-collapsed duplicate discharge

Summary of effect kinds

Program Control

Value References

​Effect contracts and effect instances

​Publication effect

​When a duplicate publication is safe

​Request effect

​Inherited result contract

​When a duplicate request is safe

​External effect

​ErrorDisposition values

​Effect intents

​Transition-owned intents

​Idempotency key propagation

​Result bindings on effect execution

​Outbox write effect

​Producer-suppressed versus consumer-collapsed duplicate discharge

​Summary of effect kinds

Program Control

Value References

Effect contracts and effect instances

Publication effect

When a duplicate publication is safe

Request effect

Inherited result contract

When a duplicate request is safe

External effect

`ErrorDisposition` values

Effect intents

Transition-owned intents

Idempotency key propagation

Result bindings on effect execution

Outbox write effect

Producer-suppressed versus consumer-collapsed duplicate discharge

Summary of effect kinds