Conseqa Operation Program: All Steps and Control Flow

The program field of an operation defines its explicit control flow as an ordered block of steps. Every step in the program describes a causal action, running an inline transaction, executing an inline effect, making a decision, and every reachable path through the program ends at an explicit terminal. There are no loops; the program structure is acyclic by construction. Transactions and direct effect contracts live inside the program at the step that executes them. There is no operation-level registry to reference back into. A retry traverses the same declared control from the first step. What the retry re-encounters at each transaction or effect step is judged by the replay and idempotency rules the verifier applies to that step.

Program structure

The program is a nested block of OperationStep values. Decision steps, match_result and branch, each open two sub-blocks (arms), and the verifier analyzes every path through the complete tree.

program:
  steps:
    - kind: transaction
      id: tx.create_order.new
      data_model: data.checkout
      isolation: read_committed
      idempotency:
        kind: deduplicated_by
        key:
          components:
            - source: input:input.create_order.request
              path: idempotency_key
      steps:
        - kind: insert
          object: object.order
          values:
            kind: deterministic
            from:
              - source: input:input.create_order.request
                path: order_id
        - 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
    - kind: execute_effect_intent
      intent: intent.create_order.publish_created
    - kind: return
      request: input.create_order.request
      outcome:
        kind: ok
        values:
          kind: deterministic
          from:
            - source: input:input.create_order.request
              path: order_id

Step kinds

`transaction`

Declares and executes one inline atomic transaction at this point in the program. On re-encounter with a keyed commit, resolves the prior Commit(operation, T.id, K) and restores its artifacts instead of executing the body again.

- kind: transaction
  id: tx.create_order.new
  data_model: data.checkout
  isolation: read_committed
  idempotency:
    kind: deduplicated_by
    key:
      components:
        - source: input:input.create_order.request
          path: idempotency_key
  steps:
    - kind: insert
      object: object.order
      values: ...

required

Stable logical ID for this inline transaction. Identifies the inline declaration itself (used for keyed commit identity, diagnostics, and proof evidence). Must be unique across all inline transactions in the operation.

Id | null

required

The transactional state boundary. null only when the transaction performs no application object access and exists solely to produce framework artifacts.

string

required

The isolation guarantee: unspecified, read_committed, snapshot, or serializable.

object

required

Keyed commit deduplication contract: unspecified, not_deduplicated, or deduplicated_by { key }.

list[TransactionStep]

required

Ordered transaction body (reads, writes, inserts, deletes, locks, transitions, effect-intent establishments, transaction-output establishments). See Transactions.

For a transaction with idempotency: { kind: deduplicated_by, key: ... }, if a prior commit exists for the same evaluated key, this step resolves that commit and restores all artifacts it retained, transaction outputs and effect intents, without executing the transaction body again. For a transaction without a keyed commit, the body executes.

`execute_effect`

Declares one inline effect contract and executes it directly at this point in the program.

- kind: execute_effect
  effect_id: effect.transcode_video.engine
  effect:
    kind: external
    name: transcoding-engine.render
    idempotency:
      kind: deduplicated_by
      key:
        components:
          - source: input:input.transcode_video.uploaded
            path: video_id
    result:
      ok: schema.RenderCompleted
      err:
        schema: schema.RenderFailed
        disposition: terminal
  values:
    kind: deterministic
    from:
      - source: input:input.transcode_video.uploaded
        path: video_id
      - source: input:input.transcode_video.uploaded
        path: source_uri
  bind: result.transcode_video.render

required

Stable identifier for this inline effect site. Used as ValueSource::Effect(effect_id) in idempotency-key propagation and other value lineage. Must be unique across inline operation-owned effect sites within the operation.

Effect

required

The inline effect contract: a publication, request, or external effect declared in full at this site. See Effects.

Derivation

required

Declares the provenance of the complete outgoing effect payload. Either kind: unspecified (unknown provenance, declared explicitly) or kind: deterministic with a from list of value references. See Value References.

Binds the effect’s synchronous result observation under this name. Only valid for result-bearing effects (request and external effects with a declared result). Publications have no result and must not declare bind. Omit when you deliberately ignore the result.

Both the effect-contract value roots and the values derivation are evaluated in the operation-level value context immediately before this step. They may not reference transaction_read bindings, which are local to the transaction that produced them.

`execute_effect_intent`

Executes an already-established effect intent. The values were fixed when the intent was established; this step runs that fixed instance without recomputing anything.

- kind: execute_effect_intent
  intent: intent.create_order.publish_created

# With an optional result binding (for a request or external intent):
- kind: execute_effect_intent
  intent: intent.transcode_video.completed
  bind: result.transcode_video.completed

required

The intent binding to execute. Must have been established by an establish_effect_intent or by a transition step’s effect_intents map on every path reaching this step (definite availability).

Optional result binding, following the same rules as for execute_effect.

`match_result`

Destructures a bound effect result into its ok and err arms. Use this step to branch on the outcome of a request or external effect; do not use branch for this purpose.

- kind: match_result
  result: result.transcode_video.render
  ok:
    steps:
      - kind: transaction
        id: tx.transcode_video.complete
        data_model: data.videos
        isolation: read_committed
        idempotency: { kind: unspecified }
        steps: [...]
      - kind: execute_effect_intent
        intent: intent.transcode_video.completed
      - kind: complete
  err:
    steps:
      - kind: transaction
        id: tx.transcode_video.fail
        data_model: data.videos
        isolation: read_committed
        idempotency: { kind: unspecified }
        steps: [...]
      - kind: complete

required

The result binding to destructure. Must be bound by an execute_effect or execute_effect_intent step on every path reaching this step.

OperationBlock

required

The block to execute when the result is Ok. Inside this block, effect_result_ok:<result> is available as a value source.

OperationBlock

required

The block to execute when the result is Err. Inside this block, effect_result_err:<result> is available as a value source.

The match is exhaustive and mutually exclusive. Both arms must be declared, though either may be empty. Variant payloads are arm-local: effect_result_ok and effect_result_err do not survive the join after the match. If data from the result must be available after the match, export it through a transaction output inside the arm.

Use match_result only for destructuring a synchronous effect result. Use branch for ordinary value comparisons. The two step kinds are not interchangeable.

`branch`

An ordinary control decision over modeled values. Executes the then block when the condition holds; optionally executes the otherwise block when it does not.

- kind: branch
  condition:
    kind: eq
    value:
      source: input:input.checkout
      path: region
    equals: CA
  then:
    steps:
      - kind: execute_effect
        effect_id: effect.checkout.apply_ca_tax
        effect:
          kind: external
          name: tax-service.apply
          idempotency: { kind: unspecified }
          result: null
        values:
          kind: unspecified
      - kind: complete
  otherwise:
    steps:
      - kind: complete

Condition

required

The predicate to evaluate. One of four forms, see Conditions below.

OperationBlock

required

The block to execute when the condition holds.

OperationBlock

The block to execute when the condition does not hold. If absent, the branch falls through to the following step. A branch without otherwise does not terminate its path, the validation rule requires every reachable path to end at a terminal.

Conditions

Kind	Description	Deterministic?
`unspecified`	No fact about how the decision is made. The verifier treats it as unknown.	No
`eq`	Equality of a value reference against `equals` (a literal scalar or another value reference).	Yes
`and`	All nested conditions hold.	Yes, if every nested condition is
`not`	The nested condition does not hold.	Yes, if the nested condition is

eq, and, and not are deterministic functions of their references. unspecified is never deterministic. A condition is deterministic only when every component is, a single unspecified anywhere in an and or not makes the whole condition unspecified. For eq, the equals field accepts either a plain scalar literal or a value reference map:

# Literal
condition:
  kind: eq
  value:
    source: input:input.checkout
    path: status
  equals: pending

# Another value reference (map form)
condition:
  kind: eq
  value:
    source: input:input.checkout
    path: order_id
  equals:
    source: transaction_output:output.lookup_order
    path: order_id

`return`

Terminates a request-driven execution by constructing the named request input’s declared result. Only valid for operations with a request input; subscription-driven operations use complete.

- kind: return
  request: input.create_order.request
  outcome:
    kind: ok
    values:
      kind: deterministic
      from:
        - source: transaction_output:output.create_order
          path: order_id
        - source: transaction_output:output.create_order
          path: status

# Returning an error outcome:
- kind: return
  request: input.create_order.request
  outcome:
    kind: err
    values:
      kind: unspecified

required

The operation-owned request input whose result contract to return. Must be a kind: request input.

string

required

Either ok (constructs the input’s ok schema payload) or err (constructs the err schema payload).

Derivation

required

Provenance of the result payload. Use kind: unspecified when provenance is unknown; never omit this field.

`complete`

Terminates an execution that returns nothing. Natural for subscription-driven operations.

- kind: complete

complete takes no parameters. Every reachable path in a subscription-driven operation must end at a complete step.

Validation rules

The verifier enforces these structural rules before any replay analysis:

Every reachable path ends at a terminal. A return or complete must be reachable from every branch. A branch without otherwise is not a valid terminal for its path.
No step follows a terminal. Steps after return or complete in the same block are unreachable and reported as errors.
IDs are unique within the operation. Duplicate Transaction.id, duplicate inline effect_id, and duplicate binding IDs are rejected.
Bindings have exactly one producer and are definitely available at every consumer. A transaction output, an effect intent, or an effect result may only be consumed at a program point where a producer has bound it on every falling-through path reaching that point.
Transaction reads never leave their transaction. A transaction_read binding is visible only inside the transaction that produced it.
Variant scope is respected. effect_result_ok:<r> is valid only inside the ok arm of a match_result on r; effect_result_err:<r> only inside the err arm.
Return targets request inputs. return.request must name a kind: request input of the operation.

Bindings do not forward-reference: a binding is unavailable before its producer step. The validator reports a use-before-bind error rather than resolving an operation-wide declaration and hoping control eventually produces the value.

Step location notation

Steps carry no location IDs of their own. Diagnostics, proofs, and the visualizer identify steps by their location: a dot-separated sequence of one-based positions and arm names.

Location	Meaning
`2`	The second top-level step
`3.ok.1`	The first step of the `ok` arm of the third top-level step
`2.then.1`	The first step of the `then` arm of the second top-level step (a `branch`)
`4.err.2`	The second step of the `err` arm of the fourth top-level step

When a proof or an obstacle is reported at a location, the same location notation appears in the JSON report’s evidence and summary fields and in the visualization. StepLocation names the site’s position in the program; keyed commit identity for a transaction is anchored on its id, not on StepLocation.

Decision replay

When the verifier analyzes idempotency or result-replay requirements, it must establish that every decision on the path replays, that every attempt in the same logical class takes the same arm. A decision replays when:

for branch: the condition is deterministic (no unspecified anywhere) and every value reference it observes is replay-stable, or
for match_result: the matched result is replay-stable.

If a decision cannot be established to replay, the verifier reports it as an obstacle. This means a retry might take a different arm, doing different work on repeated attempts. It is not proof that the decision is wrong, it is an honest gap in the model’s declared facts.

Complete example: transcode operation

The following program from the video streaming fixture shows a match_result decision and three inline transactions used across the two arms:

program:
  steps:
    # Step 1: claim the transcode job transactionally
    - kind: transaction
      id: tx.transcode_video.claim
      data_model: data.videos
      isolation: read_committed
      idempotency:
        kind: deduplicated_by
        key:
          components:
            - source: input:input.transcode_video.uploaded
              path: event_id
      steps: [...]
    # Step 2: call the transcoding engine; bind the result
    - kind: execute_effect
      effect_id: effect.transcode_video.engine
      effect:
        kind: external
        name: transcoding-engine.render
        idempotency:
          kind: deduplicated_by
          key:
            components:
              - source: input:input.transcode_video.uploaded
                path: video_id
        result:
          ok: schema.RenderCompleted
          err:
            schema: schema.RenderFailed
            disposition: terminal
      values:
        kind: deterministic
        from:
          - source: input:input.transcode_video.uploaded
            path: video_id
          - source: input:input.transcode_video.uploaded
            path: source_uri
      bind: result.transcode_video.render
    # Step 3: branch on the engine's result
    - kind: match_result
      result: result.transcode_video.render
      ok:
        steps:
          # Step 3.ok.1 — record the manifest
          - kind: transaction
            id: tx.transcode_video.complete
            data_model: data.videos
            isolation: read_committed
            idempotency: { kind: unspecified }
            steps: [...]
          # Step 3.ok.2 — announce completion
          - kind: execute_effect_intent
            intent: intent.transcode_video.completed
          # Step 3.ok.3
          - kind: complete
      err:
        steps:
          # Step 3.err.1 — mark the job failed
          - kind: transaction
            id: tx.transcode_video.fail
            data_model: data.videos
            isolation: read_committed
            idempotency: { kind: unspecified }
            steps: [...]
          # Step 3.err.2
          - kind: complete

Effects

How to declare inline effect contracts at execution and establishment sites

Value References

How to write values derivations and condition roots in program steps

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Conseqa Operation Program: All Steps and Control Flow

Program structure

Step kinds

`transaction`

`execute_effect`

`execute_effect_intent`

`match_result`

`branch`

Conditions

`return`

`complete`

Validation rules

Step location notation

Decision replay

Complete example: transcode operation

Effects

Value References

​Program structure

​Step kinds

​transaction

​execute_effect

​execute_effect_intent

​match_result

​branch

​Conditions

​return

​complete

​Validation rules

​Step location notation

​Decision replay

​Complete example: transcode operation

Effects

Value References

Program structure

Step kinds

`transaction`

`execute_effect`

`execute_effect_intent`

`match_result`

`branch`

Conditions

`return`

`complete`

Validation rules

Step location notation

Decision replay

Complete example: transcode operation