Conseqa Transactions: Idempotency, Isolation, and Steps

A transaction is one atomic commit/abort unit, declared inline at the program step that executes it. Its id is a stable logical identity unique within the operation: it carries keyed commit identity, value lineage, diagnostics, conformance, proof evidence, and visualization. Moving an inline transaction must not silently change its durable commit identity.

Transaction declaration

- kind: transaction
  id: tx.create_order
  data_model: data.orders
  isolation: serializable
  idempotency:
    kind: deduplicated_by
    key:
      components:
        - source: input:input.create_order.request
          path: request_id
  steps:
    ...

`data_model`

data_model: <id> means the transaction operates against the identified logical transactional state boundary. Object reads, writes, locks, inserts, deletes, and transitions must refer to objects belonging to that data model. data_model: null is permitted when the transaction performs no application DataObject access and only produces or consumes framework transaction artifacts. It must not be used to imply atomic application-object access with no declared transactional boundary.

Transaction body steps

The ordered body may contain:

read : Observes selected object instances. Binds the observation transaction-locally under bind.
write : Mutates selected fields. Declares value provenance through Derivation.
insert : Creates a new instance. Value provenance is declared through Derivation; object identity is not redeclared.
delete : Deletes selected instances.
transition : Selects a persistent machine instance and applies a named state-machine transition. See State machines.
lock : An explicit synchronization guarantee, acquired at the step and held until transaction termination.
establish_transaction_output : Exports a typed value into the enclosing operation’s control.
establish_effect_intent : Captures an effect instance as a transaction artifact for later execution.
write_outbox : The sole legal execution site for an OutboxWriteEffect.

The `write_outbox` step

- 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

A write_outbox step is an effect execution site, not a persistent-object insertion. Reaching the step constructs one logical message instance, evaluates values in the transaction context, and stages the admission. The destination outbox must exist, belong to the transaction’s declared data model, and admit the written schema. It executes only as a transaction step. It is the sole legal execution site for OutboxWriteEffect; it is rejected under execute_effect, execute_effect_async, establish_effect_intent, and among a transition’s side effects. It has no synchronous result, no bind, and no async variant. The transaction alone determines whether the staged write commits.

Atomicity

The staged admission participates in the containing transaction’s atomicity:

T aborts   =>  no mutation commits AND the message is not admitted
T commits  =>  the mutations commit AND the message is durably admitted

There is no state where the commit succeeds without the admission, or an admission survives an abort. A transaction declared DeduplicatedBy(K) bounds its contained writes: an already-resolved Commit(T,K) does not commit the body again, so no further committed occurrence of the write exists.

Isolation levels

unspecified : No isolation fact may be assumed.
read_committed : Reads do not observe uncommitted writes from other transactions. The verifier must still consider anomalies such as non-repeatable reads and concurrent read/modify/write races unless prevented by stronger facts.
snapshot : A transaction reads from one consistent committed snapshot for ordinary reads. Write skew and predicate-level anomalies remain possible unless ruled out by additional facts.
serializable : Committed transactions admit an equivalent serial execution order. Serializable does not by itself imply real-time precedence, and does not imply replayability across separate invocation attempts.

Transaction idempotency guarantee

A transaction exposes an IdempotencyGuarantee independently of any transaction-output or effect-intent declaration.

unspecified : No explicit keyed transaction-commit deduplication fact is available. The analyzer may still prove natural replayability from the transaction’s declared semantics.
not_deduplicated : The architecture explicitly declares that the execution environment provides no keyed transaction-commit deduplication. The analyzer may still prove natural replayability.
deduplicated_by { key } : The execution environment guarantees a durable logical commit identity Commit(T,K). At most one logical execution may successfully commit. On the first successful execution, application state, Commit(T,K), and the exact transaction artifacts commit atomically. If Commit(T,K) already exists on a later encounter, the prior logical commit is resolved and its retained artifacts are restored.

Natural replayability

Natural replayability is derived, not declared. A transaction is naturally replayable only when the verifier can establish that another execution for the same logical invocation can safely reproduce the same logical transaction outcome and any artifacts required by later program steps. This is stronger than merely showing that a second commit cannot happen. A one-shot guard that makes a second attempt abort may establish at-most-once commit behavior while still preventing the program from reconstructing artifacts after a crash. Such a guard does not, by itself, prove natural replayability.

Artifact replay after a transaction

For an artifact required after a crash, V1 accepts either:

A. reconstruction
   establishing transaction naturally replayable
   +
   artifact derivation replay-deterministic

OR

B. recovery
   establishing transaction DeduplicatedBy(K)
   +
   artifact retained by Commit(T,K)

Otherwise the artifact’s retry availability and consistency are not proven.

Transition transactions are never naturally replayable

A transaction containing any Transition is not naturally replayable under the current replay proof rules. A successful transition changes the state against which its own precondition was evaluated, so re-executing the transaction cannot generally be assumed to reproduce the same outcome or artifacts. This is a proof fact, not a structural validity rule. A transition-containing transaction may declare any IdempotencyGuarantee permitted for other transactions, and deduplicated_by { key } provides the durable recovery route: after the first successful logical commit, a later same-key encounter resolves the prior commit and restores the exact retained artifacts.

For state machine specifics, including how transition side effects are implicitly established as effect-intent artifacts, see State machines.

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Conseqa Transactions: Idempotency, Isolation, and Steps

Transaction declaration

`data_model`

Transaction body steps

The `write_outbox` step

Atomicity

Isolation levels

Transaction idempotency guarantee

Natural replayability

Artifact replay after a transaction

Transition transactions are never naturally replayable

​Transaction declaration

​data_model

​Transaction body steps

​The write_outbox step

​Atomicity

​Isolation levels

​Transaction idempotency guarantee

​Natural replayability

​Artifact replay after a transaction

​Transition transactions are never naturally replayable

Transaction declaration

`data_model`

Transaction body steps

The `write_outbox` step

Atomicity

Isolation levels

Transaction idempotency guarantee

Natural replayability

Artifact replay after a transaction

Transition transactions are never naturally replayable