> ## Documentation Index
> Fetch the complete documentation index at: https://docs.conseqa.umran.ca/llms.txt
> Use this file to discover all available pages before exploring further.
# Conseqa Operation Program: All Steps and Control Flow
> Reference for the operation program field: all step kinds, decision steps, terminal steps, step location notation, and decision replay analysis.
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.
```yaml theme={null}
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.
```yaml theme={null}
- 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.
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.
```yaml theme={null}
- 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
```
The ID of the effect to execute. Must be declared in the operation's `effects` map.
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](/dsl/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.
```yaml theme={null}
- kind: execute_effect_intent
intent: intent.create_order.publish_created
```
```yaml theme={null}
# 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
```
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.
```yaml theme={null}
- 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
```
The result binding to destructure. Must be bound by an `execute_effect` or `execute_effect_intent` step on every path reaching this step.
The block to execute when the result is `Ok`. Inside this block, `effect_result_ok:` is available as a value source.
The block to execute when the result is `Err`. Inside this block, `effect_result_err:` 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.
```yaml theme={null}
- 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
```
The predicate to evaluate. One of four forms — see [Conditions](#conditions) below.
The block to execute when the condition holds.
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:
```yaml theme={null}
# 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`.
```yaml theme={null}
- 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
```
```yaml theme={null}
# Returning an error outcome:
- kind: return
request: input.create_order.request
outcome:
kind: err
values:
kind: unspecified
```
The operation-owned request input whose result contract to return. Must be a `kind: request` input.
Either `ok` (constructs the input's `ok` schema payload) or `err` (constructs the `err` schema payload).
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.
```yaml theme={null}
- 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:
1. **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.
2. **No step follows a terminal.** Steps after `return` or `complete` in the same block are unreachable and reported as errors.
3. **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.
4. **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.
5. **Variant scope is respected.** `effect_result_ok:` is valid only inside the `ok` arm of a `match_result` on `r`; `effect_result_err:` only inside the `err` arm.
6. **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:
```yaml theme={null}
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
```
How to declare the effects that program steps execute
How to write values derivations and condition roots in program steps