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 a transaction, executing an 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. 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
      transaction: tx.create_order.new
    - 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: transaction_output:output.create_order
              path: order_id
            - source: transaction_output:output.create_order
              path: status

Step kinds

`transaction`

Executes, or resolves the prior keyed commit of, an operation-owned transaction.

- kind: transaction
  transaction: tx.create_order.new

For a transaction with idempotency: { kind: deduplicated_by, key: ... }, if a prior Commit(T,K) 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.

required

The ID of the transaction to run. Must be declared in the operation’s transactions map.

`execute_effect`

Constructs one instance of an operation-owned effect and executes it directly.

- kind: execute_effect
  effect: effect.transcode_video.engine
  values:
    kind: deterministic
    from:
      - source: input:input.transcode_video.uploaded
        path: video_id
      - source: input:input.transcode_video.uploaded
        path: source_uri
  result: result.transcode_video.render

required

The ID of the effect to execute. Must be declared in the operation’s effects map.

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 under this ID. Only valid for result-bearing effects (request and external effects with a declared result). Publications have no result and must not declare one. Omit when you deliberately ignore the result.

The derivation is evaluated in the operation-level value context. It may not reference transaction_read results, 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
  result: result.transcode_video.completed

required

The ID of the effect intent to execute. Must be declared in the operation’s effect_intents map and be definitely available at this program point — established or recovered on every path reaching here.

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
        transaction: tx.transcode_video.complete
      - kind: execute_effect_intent
        intent: intent.transcode_video.completed
      - kind: complete
  err:
    steps:
      - kind: transaction
        transaction: tx.transcode_video.fail
      - 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: effect.checkout.apply_ca_tax
        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.
Transaction artifacts are definitely available. A transaction output or effect intent may only be consumed at a program point where a transaction on every path reaching that point has established or recovered it.
Result bindings are definitely assigned. A result binding may only be matched or referenced where an effect-executing step has bound it on every path reaching that point.
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.

Step location notation

Steps carry no IDs. 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.

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 both a match_result decision and three transactions used across the two arms:

program:
  steps:
    # Step 1: claim the transcode job transactionally
    - kind: transaction
      transaction: tx.transcode_video.claim
    # Step 2: call the transcoding engine; bind the result
    - kind: execute_effect
      effect: effect.transcode_video.engine
      values:
        kind: deterministic
        from:
          - source: input:input.transcode_video.uploaded
            path: video_id
          - source: input:input.transcode_video.uploaded
            path: source_uri
      result: 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
            transaction: tx.transcode_video.complete
          # 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
            transaction: tx.transcode_video.fail
          # Step 3.err.2
          - kind: complete

Effects

How to declare the effects that program steps execute

Value References

How to write values derivations and condition roots in program steps

Get Started

Core Concepts

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