An Operation is a declared, persona-gated, precondition-guarded unit of work that produces entity state transitions as its sole side effect and declares a finite set of named outcomes. Operations are the only construct in the evaluation model that produces side effects.

DSL Syntax

operation <OperationId> {
  personas: [<PersonaId>, ...]
  require:  <PredicateExpression>
  effects:  [<EntityId>: <from_state> -> <to_state>, ...]
  outcomes: [<OutcomeLabel>, ...]
}

Fields

Field	Required	Description
personas	Yes	Non-empty set of personas that may invoke this operation.
require	Yes	A predicate expression over the ResolvedVerdictSet and FactSet. See Symbols & Operators for the predicate grammar.
effects	Yes	Entity state transitions as EntityId: from_state -> to_state tuples.
outcomes	Yes	Named success-path results. At least one outcome is required.

Execution Sequence

The execution sequence is fixed and invariant. No step may be reordered or skipped:

1. Persona check. Is persona in op.allowed_personas? If not, return Error("persona_rejected").
2. Precondition evaluation. Does eval_pred(op.precondition, FactSet, verdict_set) return true? If not, return Error("precondition_failed").
3. Outcome determination. Determine which declared outcome to produce based on entity state and effect-to-outcome mapping.
4. Atomic effect application. Apply all effects associated with the determined outcome atomically. Either all transitions succeed or none do.
5. Provenance emission. Record the persona, verdicts used, entity state before/after, and outcome label.

The executor validates that the current entity state matches the transition source for each effect (obligation E2). A mismatched transition source aborts the operation.

Single-Outcome Operations

Most operations have a single outcome:

operation confirm_order {
  personas: [warehouse_manager]
  require:  verdict_present(inventory_available)
  effects:  [Order: pending -> confirmed]
  outcomes: [confirmed]
}

For single-outcome operations, effect-to-outcome association is implicit -- all effects belong to the sole outcome.

Multi-Outcome Operations

When an operation can produce different success results, declare multiple outcomes with effect-to-outcome associations:

operation decide_claim {
  personas: [adjudicator]
  require:  verdict_present(claim_eligible)
  outcomes: [approved, rejected]
  effects:  [
    Claim: review -> approved  -> approved,
    Claim: review -> rejected  -> rejected
  ]
}

In the multi-outcome form, each effect tuple is extended with -> OutcomeLabel to declare which outcome it belongs to. All effects for a given outcome are applied atomically when that outcome is produced.

The outcome is determined by the effect-to-outcome mapping declared in the contract -- the executor matches the current entity state against the declared effect source states and selects the outcome whose associated effects are applicable. This is not executor discretion.

Multiple Effects (Cross-Entity)

An operation can transition multiple entities simultaneously:

operation finalize_trade {
  personas: [trade_admin]
  require:  verdict_present(all_checks_passed)
  effects:  [
    Trade:      pending -> finalized,
    Settlement: awaiting -> processing
  ]
  outcomes: [finalized]
}

All effects are applied atomically (executor obligation E3). If any entity is not in the expected state, none of the transitions occur.

No Wildcard Transitions

Every effect must name an explicit source state and target state. Wildcard notation is not permitted:

// WRONG -- wildcard source not permitted
operation reject_requisition {
  personas: [approver]
  require:  true
  effects:  [Requisition: * -> rejected]
}

Operations invocable from multiple source states must declare multiple explicit effects:

// CORRECT -- explicit effects for each source state
operation reject_requisition {
  personas: [approver]
  require:  true
  effects:  [
    Requisition: submitted -> rejected,
    Requisition: manager_approved -> rejected,
    Requisition: dept_review -> rejected
  ]
  outcomes: [rejected]
}

This requirement enables E2 source-state validation -- the executor can verify exactly which transitions are legal.

Error Types

Operations declare error types that cover the three failure modes:

Error	Cause
persona_rejected	The requesting persona is not in allowed_personas.
precondition_failed	The precondition evaluated to false.
InvalidEntityState	The entity's current state does not match the effect's source state (E2 violation at runtime).

Atomicity is an executor obligation (E3). Either all declared state transitions for the produced outcome occur, or none do. Partial application is not permitted.

S3a -- Structural Admissibility

Static analysis S3a determines, for each entity state and persona, which operations are structurally satisfiable. This is type-level analysis: a precondition comparing a Bool fact to "premium" (a string) is structurally unsatisfiable. A precondition comparing two compatible types is structurally satisfiable.

S3a: For each Entity state S, Persona P:
  { op | P in op.allowed_personas
    AND op.effects include a transition from S
    AND op.precondition is structurally satisfiable }

This analysis is O(|expression tree|) per precondition and is always computationally feasible.

Full Working Example

A complete contract with single and multi-outcome operations:

// --- Personas ---
persona applicant
persona underwriter
persona compliance_officer

// --- Entities ---
entity LoanApplication {
  states:  [submitted, under_review, approved, denied, compliance_hold]
  initial: submitted
  transitions: [
    (submitted, under_review),
    (under_review, approved),
    (under_review, denied),
    (under_review, compliance_hold),
    (compliance_hold, approved),
    (compliance_hold, denied)
  ]
}

// --- Facts ---
fact credit_score {
  type:   Int(min: 300, max: 850)
  source: "credit_bureau.score"
}

fact loan_amount {
  type:   Money(currency: "USD")
  source: "application_service.requested_amount"
}

fact income_verified {
  type:    Bool
  source:  "verification_service.income_confirmed"
  default: false
}

fact compliance_flag {
  type:    Bool
  source:  "compliance_engine.flagged"
  default: false
}

// --- Rules ---
rule credit_acceptable {
  stratum: 0
  when:    credit_score >= 620
  produce: verdict credit_ok { payload: Bool = true }
}

rule income_confirmed {
  stratum: 0
  when:    income_verified = true
  produce: verdict income_ok { payload: Bool = true }
}

rule eligible_for_review {
  stratum: 1
  when:    verdict_present(credit_ok) and verdict_present(income_ok)
  produce: verdict review_eligible { payload: Bool = true }
}

// --- Operations ---

// Single-outcome: begin review
operation begin_review {
  personas: [underwriter]
  require:  verdict_present(review_eligible)
  effects:  [LoanApplication: submitted -> under_review]
  outcomes: [in_review]
}

// Multi-outcome: underwriter decides
operation decide_application {
  personas: [underwriter]
  require:  verdict_present(review_eligible)
  outcomes: [approved, denied, held]
  effects:  [
    LoanApplication: under_review -> approved         -> approved,
    LoanApplication: under_review -> denied            -> denied,
    LoanApplication: under_review -> compliance_hold   -> held
  ]
}

// Compliance officer resolves hold
operation resolve_hold {
  personas: [compliance_officer]
  require:  true
  outcomes: [approved, denied]
  effects:  [
    LoanApplication: compliance_hold -> approved  -> approved,
    LoanApplication: compliance_hold -> denied    -> denied
  ]
}

Provenance

Every operation execution produces a provenance record:

OperationProvenance = (
  op:               OperationId,
  persona:          PersonaId,
  outcome:          OutcomeLabel,
  instance_binding: Map<EntityId, InstanceId>,
  facts_used:       Set<FactId>,
  verdicts_used:    ResolvedVerdictSet,
  state_before:     Map<(EntityId, InstanceId), StateId>,
  state_after:      Map<(EntityId, InstanceId), StateId>
)

The outcome field enables provenance chains to track not just state transitions but which success-path result led to subsequent flow routing decisions.

Constraints

• An operation with an empty allowed_personas set is a contract error: "allowed_personas must be non-empty".
• Every PersonaId in allowed_personas must resolve to a declared Persona. Violations: "undeclared persona '<id>'".
• Each effect must reference a declared entity, and the transition must exist in that entity's transition relation. Violations: "effect references undeclared entity '<id>'".
• At least one outcome is required. Outcome labels must be unique within the operation.
• The outcome set and error_contract set must be disjoint.
• For multi-outcome operations, every effect must be associated with exactly one declared outcome.
• Operations do NOT produce verdict instances. Verdict production belongs exclusively to rules.

Common Mistakes

Testing entity state in preconditions. You cannot write Requisition.state = "draft" in a precondition. Entity state is not a predicate term. State constraints are enforced through effect declarations (Requisition: draft -> submitted) and E2 validation.

Missing outcomes. Every operation must declare at least one outcome. Operations without outcomes are elaboration errors.

Overlapping effects in parallel branches. Two operations in parallel branches that transition the same entity type create a conflict detected at elaboration time. Use separate entity types for independent parallel work.

Assuming operations produce verdicts. Operations produce state transitions and outcomes. Verdicts come from rules only.

How Operations Connect to Other Constructs

• Entities provide the state machines that operations transition.
• Personas gate who can invoke each operation.
• Rules produce the verdicts that operations reference in preconditions.
• Flows orchestrate operations via OperationSteps, routing on outcomes.
• Provenance records every operation execution with full traceability.

Static Analysis Properties

• S3a (Structural admissibility) determines which operations are structurally possible for each entity state and persona combination.
• S4 (Authority topology) maps personas to operations across all entity states.
• S5 (Verdict and outcome space) enumerates all possible outcomes for each operation.
• S6 (Flow path enumeration) traces operation outcomes through flow routing.