> ## 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. # Correctness Requirements in Conseqa: Proof Obligations > Requirements are proof obligations declared on operations. Learn serialization, ordering, idempotency, and recoverability, plus how verdicts are produced. Requirements are the correctness properties you want your architecture to satisfy. You declare them on operations under the `requirements` key. The verifier then attempts to prove each requirement from the facts declared elsewhere in the model — topic ordering, transaction isolation, delivery semantics, dispatch routing, and so on. Declaring a requirement says "this must hold." It does not assert that it does hold. Only a `proven` verdict does that. Declaring a requirement is not the same as proving it. Always check the verification output for the verdict (`proven`, `unknown`, or `disproven`) before relying on a correctness property in production. ## The four requirement kinds An operation's `requirements` block contains four lists. Each list is empty (`[]`) by default, meaning no obligation is declared for that property. ```yaml theme={null} requirements: serialization: [] ordering: [] idempotency: [] recoverability: [] ``` ## Serialization A serialization requirement declares that same-key invocations must not execute concurrently. ```yaml theme={null} serialization: - key: source: input:input.reserve_inventory.created path: order_id ``` `key` is a single `ValueRef` — a source and a field path. The requirement constrains only invocations triggered by the input the key is sourced from. Invocations with different key values may run concurrently; invocations with the same key value must not overlap. Serialization establishes mutual exclusion only. It does not establish which same-key invocation comes first. A non-FIFO lock or single-lane execution with any enqueue order may prove serialization without proving ordering. **Proven by:** a mechanism that prevents overlap for equal key values — for example, `by_topic_key` dispatch with `lane_concurrency: bounded(1)`, or an exclusive lock acquired before any conflicting work. ## Ordering An ordering requirement declares that same-key invocations must take effect in the semantic precedence order established by their source. ```yaml theme={null} ordering: - key: source: input:input.reserve_inventory.created path: order_id ``` Ordering is strictly stronger than serialization. A proof must establish both where the relevant precedence comes from and that the execution mechanism preserves it. Arbitrarily serializing concurrent inputs satisfies serialization but cannot invent a required semantic precedence. **V1 recognizes one precedence source:** the order declared on the key's subscription topic — a keyed topic's per-key order (when the ordering key carries the topic key for every admitted schema), or a global topic's order for any key. **The standard execution mechanism:** ```text theme={null} keyed topic ordering ↓ by_topic_key dispatch ← same-key deliveries enter one lane ↓ lane_concurrency bounded(1) ← invocations in one lane cannot overlap ``` Each declaration contributes a different fact; none substitutes for another. ## Idempotency An idempotency requirement identifies a logical invocation by a composite `IdempotencyKey` and declares that repeated attempts representing the same logical invocation must not cause externally distinguishable duplicate logical work beyond what the declared idempotency contract permits. ```yaml theme={null} idempotency: - key: components: - source: input:input.create_order.request path: idempotency_key result: replay_consistent ``` ### Idempotency key `key` is an `IdempotencyKey`: an ordered tuple of `ValueRef` components. Two attempts share the same logical invocation identity when all components evaluate to equal values. The key is a composite — not a set of alternatives. Every component must be sourced from a single input of the operation (the triggering input). A component sourced from mutable state or from an artifact the invocation itself produces cannot define a pre-execution equivalence class; such a key yields an `unknown` verdict. ### `result: replay_consistent` When `result: replay_consistent` is declared, the verifier additionally checks that repeated admitted attempts in the same idempotency class that return a request result return the same result variant and a replay-equivalent payload. Omit this or use `result: unspecified` when you need only side-effect safety, not a stable return value. ### What the verifier checks For each admitted path through the program, the verifier checks three legs: 1. **State leg.** Every transaction on the path must be retry-safe: either naturally replayable or deduplicated by a stable key. 2. **Effect leg.** Every effect-executing step must be duplicate-safe: a publication is safe when topic identity and all modeled consumers' idempotency collapse duplicates; a request is safe when the target proves its own idempotency; an external effect is safe when `deduplicated_by` with a stable key. 3. **Control leg.** Every decision on the path must replay: a `branch` condition is deterministic over replay-stable roots; a `match_result` matches a replay-stable result. The verifier computes verdicts as a greatest fixpoint across mutual dependencies between operations (publications through topics, requests to other operations), so a cycle of requirements that each collapse the others' duplicates can be proven. ## Recoverability A recoverability requirement declares that the logical invocation identified by its key must reach a valid terminal (`return` or `complete`) after any modeled interruption. ```yaml theme={null} recoverability: - key: components: - source: input:input.apply_payment.captured path: event_id completion: guaranteed ``` Recoverability is a **progress** obligation. Idempotency is a **safety** obligation. Neither implies the other. * **Idempotency without recoverability** — repeated attempts are safe, but there is no obligation to re-drive the invocation to completion. An interrupted operation that is never retried violates nothing idempotency-wise. * **Recoverability without idempotency** — the invocation must eventually reach a terminal, but repeating the work is assumed harmless. Use this when the operations are inherently safe to repeat. ### `completion: resumable` An interrupted attempt must be **able** to resume and drive the program to a terminal. The verifier checks that every already-committed transaction resolves on re-encounter (by natural replay or by `deduplicated_by` key), and that every artifact a later step consumes is replay-available. ```yaml theme={null} completion: resumable ``` `resumable` does not oblige the architecture to actually re-drive the invocation. Use it when the retry driver lies outside the model — typically a request input whose caller Conseqa does not model. ### `completion: guaranteed` In addition to resumability, the architecture must guarantee that the logical invocation **is** re-driven until the program reaches a terminal. This is a liveness obligation. ```yaml theme={null} completion: guaranteed ``` A `guaranteed` proof requires a modeled retry driver: * `delivery: at_least_once` on the triggering subscription, or * an inbound `RequestEffect` whose `retry` is `may_repeat` `guaranteed` recoverability proofs are conditional on the delivery abstraction genuinely redelivering until the invocation succeeds. `at_least_once` delivery does not encode retry timing, retry count, backoff, or a bounded eventual-delivery liveness guarantee. The proof rests on the modeled fact, subject to implementation conformance. If you declare `completion: guaranteed` on an operation that has no idempotency requirement keyed from the triggering input, the verifier emits a warning. The retry driver makes retries expected, and nothing declares them safe. ## Verdicts After running `conseqa model.yaml`, every declared requirement receives one of three verdicts: | Verdict | Meaning | | ----------- | ------------------------------------------------------------------------- | | `proven` | The requirement follows from the declared facts | | `unknown` | The verifier could not establish the requirement from the available facts | | `disproven` | The verifier found a concrete path that violates the requirement | `unknown` is **epistemic** — it means the model does not provide enough facts to complete a proof. It does not mean the implementation is actually incorrect. Respond to `unknown` by adding the missing declarations (a keyed transaction deduplication, a declared message identity, a dispatch routing fact) rather than treating the requirement as satisfied. `disproven` identifies a specific structural gap or contradiction. The obligation summary names the path and the obstacle. ## A complete requirements example The following is the full requirements block from `operation.apply_payment` in the flash checkout model. It declares serialization and ordering over `order_id` (so same-order payment applications are serialized and ordered), idempotency keyed by `event_id` (so duplicate deliveries of the same `PaymentCaptured` event are safe), and guaranteed recoverability (so the order is never left in `paid` state without the downstream effect having been attempted). ```yaml theme={null} requirements: serialization: - key: source: input:input.apply_payment.captured path: order_id ordering: - key: source: input:input.apply_payment.captured path: order_id idempotency: - key: components: - source: input:input.apply_payment.captured path: event_id result: unspecified recoverability: - key: components: - source: input:input.apply_payment.captured path: event_id completion: guaranteed ``` ## Requirements and the verification cascade Idempotency verdicts are mutually dependent: a publication effect is safe only when every modeled consumer collapses duplicates, and a request effect is safe only when the target proves its own idempotency. The verifier computes all verdicts together as a greatest fixpoint. A cycle of requirements that each collapse the others' duplicates is marked `proven (coinductive)` — the proof rests on the mutual assumption, which is sound by a minimal-counterexample argument. The same fixpoint governs `result: replay_consistent` requirements through request chains. A proof of replay consistency in one operation may depend on replay consistency in the operation it calls, and vice versa.