Conseqa Operations: Inputs, Programs, and Effects

An operation is a logical unit of application behavior owned by one service. It declares possible invocation sources, one explicit causal program, and requirements. Everything created during execution (transactions, effects, outputs, intents, async handles) is declared inline at the site that creates it.

Operation fields

An operation contains exactly these fields:

service : The owning service.
description : Documentation only; no proof semantics.
inputs : Possible invocation sources. See the three input kinds below.
program : The single explicit causal control structure.
requirements : Proof obligations the verifier must discharge.

There is no execution.concurrency field on an operation. Runtime concurrency is declared exclusively by ExecutionPool.member_concurrency in the optional L1 runtime layer.

Three input kinds

Request input

A request input declares a directly invoked operation input and the schema of its payload.

inputs:
  input.create_order.request:
    kind: request
    schema: schema.CreateOrderRequest
    identity:
      kind: keyed
      fields:
        - request_id
    result:
      ok: schema.CreateOrderResponse
      err:
        schema: schema.RequestRejected
        disposition: unspecified

identity declares where the identity of one logical request lives in the payload. keyed guarantees that any two requests whose identity field values are equal present equal payloads. unspecified provides no such fact. result declares the Result<Ok, Err> contract returned by this input. disposition is terminal, retryable, or unspecified.

Subscription input

A subscription declares invocation from a topic.

inputs:
  input.order_created:
    kind: subscription
    topic: topic.order_events
    messages: all
    acknowledge_on_success: true

Its L0 content is the topic and the selected message schemas. It does not carry delivery or dispatch; those are L1 facts declared in a SubscriptionRuntime.

Outbox input

An outbox input declares invocation from a committed outbox message.

inputs:
  input.publish_order_event:
    kind: outbox
    outbox: outbox.order_events
    messages:
      - schema.OrderCreated
      - schema.OrderPaid
    acknowledge_on_success: true

Its L0 content is the outbox, the selected message schemas, and an explicit acknowledge_on_success declaration. Like subscriptions, it carries no delivery or dispatch facts; those live in an OutboxRuntime.

The program

operation.program is the operation’s single control structure: a block of steps executed in order, with match_result and branch decisions nesting further blocks. Every reachable path ends at return (for a request input) or complete (returning nothing). The structure is acyclic by construction: no loops exist. Asynchronous effect steps may initiate effect executions whose lifetimes overlap later control, and join_all / race add explicit completion dependencies, but the operation remains a control-flow DAG plus effect-completion edges. Control flow describes causality. It is not a durable workflow, a checkpoint, or a program counter: a retry traverses the same declared control from the first step, and what it re-encounters is judged by transaction and effect replay rules.

For details on async effect steps and synchronization, see Async effects. For the full program step vocabulary, see Program control.

Stable execution-site IDs versus bindings

Two kinds of names arise from inline declarations, and they are not the same thing. Stable execution-site IDs identify the inline declaration itself:

Transaction.id
ExecuteEffect.effect_id
EstablishEffectIntent.effect_id

These IDs do not reference another declaration. They are used for keyed commit identity, value lineage, diagnostics, conformance, proof evidence, and visualization. A step’s location in the program is not a substitute: moving an inline transaction must not silently change its durable commit identity. Bindings name something produced by execution:

a transaction read observation
a transaction output artifact
an effect-intent artifact
an effect result observation
an async handle

Bindings are immutable, single-producer, operation-local, and scoped by program and transaction structure. There is no rebinding, no shadowing, and no forward reference. An async launch therefore carries two independently meaningful names: effect_id, the stable identity of the inline effect occurrence, and handle, an invocation-local synchronization artifact naming one asynchronous execution occurrence.

Compact example

operations:
  op.create_order:
    service: svc.orders
    description: Create a new order
    inputs:
      input.create_order.request:
        kind: request
        schema: schema.CreateOrderRequest
        result:
          ok: schema.CreateOrderResponse
          err:
            schema: schema.RequestRejected
            disposition: unspecified
    program:
      steps:
        - kind: transaction
          id: tx.create_order
          data_model: data.orders
          isolation: serializable
          steps:
            - kind: write_outbox
              effect_id: effect.create_order.outbox_created
              effect:
                outbox: outbox.order_events
                schema: schema.OrderCreated
                idempotency_key_propagation: []
              values:
                kind: deterministic
                from:
                  - source: input:input.create_order.request
                    path: order_id
            - kind: establish_transaction_output
              bind: output.create_order
              schema: schema.CreateOrderResponse
              values:
                kind: deterministic
                from:
                  - source: input:input.create_order.request
                    path: order_id
        - kind: execute_effect
          effect_id: effect.create_order.publish_event
          effect:
            kind: publication
            topic: topic.order_events
            schema: schema.OrderCreated
          values:
            kind: deterministic
            from:
              - source: transaction_output:output.create_order
                path: order_id
        - kind: return
          request: input.create_order.request
          outcome:
            kind: ok
            values:
              kind: deterministic
              from:
                - source: transaction_output:output.create_order
                  path: order_id

In this example:

The transaction writes an outbox message and establishes a transaction output.
The program publishes to a topic using the transaction output for provenance.
The operation returns an Ok result constructed from the transaction output.

If serialization is needed, it comes from L1 routing and pool facts, or from L0 transactions and locks. No operation-level concurrency declaration exists.

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Conseqa Operations: Inputs, Programs, and Effects

Operation fields

Three input kinds

Request input

Subscription input

Outbox input

The program

Stable execution-site IDs versus bindings

Compact example

​Operation fields

​Three input kinds

​Request input

​Subscription input

​Outbox input

​The program

​Stable execution-site IDs versus bindings

​Compact example

Operation fields

Three input kinds

Request input

Subscription input

Outbox input

The program

Stable execution-site IDs versus bindings

Compact example