A Rule is a stratified, verdict-producing, side-effect-free evaluation function. Rules read from facts and lower-stratum verdict outputs. They produce verdict instances. They do not modify entity state. They do not invoke operations. Rules are the decision logic of a Tenor contract.

DSL Syntax

rule <RuleId> {
  stratum: <nat>
  when:    <PredicateExpression>
  produce: verdict <VerdictName> { payload: <BaseType> = <value> }
}

Fields

Field	Required	Description
stratum	Yes	Non-negative integer. Determines what the rule can reference.
when	Yes	A predicate expression that must be true for the rule to fire. See Symbols & Operators for the complete predicate grammar.
produce	Yes	One or more verdicts emitted when the rule fires. Each verdict has a name and a typed payload.

Stratification

Rules are assigned to explicit, numbered strata. A rule in stratum N may only reference outputs from rules in strata strictly below N. No same-stratum references are permitted, regardless of whether the intra-stratum dependency graph would be acyclic.

Formally: for any rule r that references the output of rule r', stratum(r') < stratum(r). Equality is not permitted.

• Stratum 0 -- can reference only facts (ground layer)
• Stratum 1 -- can reference facts and verdicts from stratum 0
• Stratum N -- can reference facts and verdicts from strata 0 through N-1

Multiple rules may occupy the same stratum provided they have no dependencies on each other.

Re-expression theorem: Any acyclic same-stratum dependency graph can be mechanically transformed into strict stratification with no loss of expressive power. If you accidentally put dependent rules at the same stratum, the fix is always to move the dependent rule to a higher stratum.

Verdict Definition

Each verdict type has a name and a payload schema:

produce: verdict payment_ok { payload: Bool = true }
produce: verdict risk_score { payload: Int(min: 0, max: 100) = 85 }
produce: verdict threshold_amount { payload: Money(currency: "USD") = 10000.00 }

Verdicts form a finite tagged set. The payload type can be any BaseType. The payload value is the result produced when the rule fires.

Verdict Uniqueness (S8)

Each VerdictType name is produced by exactly one rule in the entire contract. If two or more rules (at any stratum) produce the same VerdictType name, the contract is statically rejected. This is structural check S8, enforced during Pass 5.

// WRONG -- two rules produce the same verdict name
rule check_a {
  stratum: 0
  when:    amount > 100
  produce: verdict approved { payload: Bool = true }
}

rule check_b {
  stratum: 0
  when:    status = "premium"
  produce: verdict approved { payload: Bool = true }  // ERROR: S8 violation
}

The correct pattern is distinct verdict names composed at a higher stratum:

rule check_a {
  stratum: 0
  when:    amount > 100
  produce: verdict amount_ok { payload: Bool = true }
}

rule check_b {
  stratum: 0
  when:    status = "premium"
  produce: verdict premium_status { payload: Bool = true }
}

rule final_approval {
  stratum: 1
  when:    verdict_present(amount_ok) and verdict_present(premium_status)
  produce: verdict approved { payload: Bool = true }
}

Predicate Expression Syntax

The when clause uses the predicate expression grammar. See Symbols & Operators for the complete operator reference including Unicode and ASCII forms.

Fact comparisons:

when: cargo_weight_kg <= 50000
when: risk_level = "high"
when: order_total > compliance_threshold

Logical connectives (and/∧, or/∨, not/¬):

when: delivery_confirmed = true and dispute_filed = false
when: verdict_present(amount_ok) or verdict_present(override_approved)
when: not verdict_present(blocked)

Verdict presence:

when: verdict_present(payment_verified)

Arithmetic (literal multiplication only -- no variable x variable in predicates):

when: base_amount + surcharge > threshold
when: unit_price * 100 <= budget_limit

Bounded quantification over List-typed facts (forall/∀, exists/∃):

when: forall item in line_items . item.amount > 0
when: exists doc in documents . doc.status = "verified"

Variable x variable multiplication is permitted only in Rule bodies (produce clauses), not in predicate expressions. This is the only location in the language where it is available:

rule compute_total_tax {
  stratum: 0
  when:    true
  produce: verdict total_tax {
    payload: Int(min: 0, max: 10000000) = item_count * unit_tax_amount
  }
}

The product range is computed from the operand fact type ranges and must be contained within the declared verdict payload type.

Rule Evaluation

eval_strata(contract, facts) =
  verdicts = empty
  for n = 0 to max_stratum:
    stratum_rules = { r in contract.rules | r.stratum = n }
    new_verdicts  = union { eval_rule(r, facts, verdicts) | r in stratum_rules }
    verdicts      = verdicts union new_verdicts
  return resolve(verdicts)

This fold terminates because the number of strata is finite and each stratum is fully evaluated before the next. Resolution is the identity on sets -- it returns the accumulated verdict set. Each VerdictType appears at most once in a conforming contract (guaranteed by S8).

Multi-Stratum Example: Healthcare Prior Authorization

From the healthcare domain, four strata build a complete authorization decision:

Stratum 0 -- ground checks against facts:

rule all_records_complete {
  stratum: 0
  when:    forall record in medical_records . record.is_complete = true
  produce: verdict records_complete { payload: Bool = true }
}

rule diagnosis_covered {
  stratum: 0
  when:    policy_criteria.diagnosis_covered = true
  produce: verdict diagnosis_is_covered { payload: Bool = true }
}

rule treatment_in_formulary {
  stratum: 0
  when:    policy_criteria.treatment_in_formulary = true
  produce: verdict treatment_is_formulary { payload: Bool = true }
}

rule provider_network_check {
  stratum: 0
  when:    policy_criteria.provider_in_network = true
  produce: verdict provider_in_network { payload: Bool = true }
}

rule step_therapy_check {
  stratum: 0
  when:    policy_criteria.step_therapy_complete = true
  produce: verdict step_therapy_done { payload: Bool = true }
}

rule records_relevant_check {
  stratum: 0
  when:    forall record in medical_records . record.is_relevant = true
  produce: verdict records_relevant { payload: Bool = true }
}

rule clinical_criteria_check {
  stratum: 0
  when:    clinical_review_score >= 70
  produce: verdict clinical_criteria_passed { payload: Bool = true }
}

Stratum 1 -- compose ground verdicts into eligibility determinations:

rule documentation_sufficient {
  stratum: 1
  when:    verdict_present(records_complete) and verdict_present(records_relevant)
  produce: verdict documentation_ok { payload: Bool = true }
}

rule policy_criteria_satisfied {
  stratum: 1
  when:    verdict_present(diagnosis_is_covered)
       and verdict_present(treatment_is_formulary)
       and verdict_present(provider_in_network)
       and verdict_present(step_therapy_done)
  produce: verdict policy_satisfied { payload: Bool = true }
}

Stratum 2 -- final authorization decision:

rule can_approve {
  stratum: 2
  when:    verdict_present(documentation_ok)
       and verdict_present(policy_satisfied)
       and verdict_present(clinical_criteria_passed)
  produce: verdict authorization_approved { payload: Bool = true }
}

rule should_deny {
  stratum: 2
  when:    verdict_present(documentation_ok)
       and not verdict_present(clinical_criteria_passed)
  produce: verdict authorization_denied { payload: Bool = true }
}

Stratum 3 -- appeal outcome:

rule can_overturn_denial {
  stratum: 3
  when:    verdict_present(appeal_meritorious)
        or verdict_present(new_evidence_available)
  produce: verdict overturn_recommended { payload: Bool = true }
}

This contract has 13 rules across 4 strata. Each verdict traces to a single source rule. The stratification makes the data flow visible: facts feed stratum 0, stratum 0 feeds stratum 1, and so on. No cycles, no ambiguity.

Payload Types

Verdict payloads can be any BaseType:

// Bool payload
produce: verdict payment_ok { payload: Bool = true }

// Int payload
produce: verdict risk_score { payload: Int(min: 0, max: 100) = 85 }

// Money payload (from variable x variable multiplication)
produce: verdict tax_amount {
  payload: Money(currency: "USD") = item_total * tax_rate
}

// Enum payload
produce: verdict risk_category {
  payload: Enum(values: [low, medium, high]) = "high"
}

Full Working Example

A complete contract with multi-stratum rules:

// --- Personas ---
persona buyer
persona seller
persona escrow_agent
persona compliance_officer

// --- Entity ---
entity EscrowAccount {
  states:  [held, released, refunded, disputed]
  initial: held
  transitions: [
    (held, released),
    (held, refunded),
    (held, disputed),
    (disputed, released),
    (disputed, refunded)
  ]
}

// --- Facts ---
fact escrow_amount {
  type:   Money(currency: "USD")
  source: "escrow_service.balance"
}

fact compliance_threshold {
  type:    Money(currency: "USD")
  source:  "compliance_db.threshold"
  default: 10000.00
}

fact delivery_confirmed {
  type:    Bool
  source:  "tracking_service.delivered"
  default: false
}

fact buyer_requested_refund {
  type:    Bool
  source:  "buyer_portal.refund_requested"
  default: false
}

// --- Rules (stratum 0: ground checks) ---
rule threshold_check {
  stratum: 0
  when:    escrow_amount <= compliance_threshold
  produce: verdict within_threshold { payload: Bool = true }
}

rule delivery_check {
  stratum: 0
  when:    delivery_confirmed = true
  produce: verdict delivery_ok { payload: Bool = true }
}

// --- Rules (stratum 1: compose ground verdicts) ---
rule auto_release_eligible {
  stratum: 1
  when:    verdict_present(within_threshold) and verdict_present(delivery_ok)
  produce: verdict can_auto_release { payload: Bool = true }
}

rule compliance_release_eligible {
  stratum: 1
  when:    not verdict_present(within_threshold) and verdict_present(delivery_ok)
  produce: verdict needs_compliance_release { payload: Bool = true }
}

// --- Operations ---
operation release_escrow {
  personas: [escrow_agent]
  require:  verdict_present(can_auto_release)
  effects:  [EscrowAccount: held -> released]
  outcomes: [released]
}

operation release_with_compliance {
  personas: [compliance_officer]
  require:  verdict_present(needs_compliance_release)
  effects:  [EscrowAccount: held -> released]
  outcomes: [released]
}

operation refund_buyer {
  personas: [escrow_agent]
  require:  buyer_requested_refund = true
  effects:  [EscrowAccount: held -> refunded]
  outcomes: [refunded]
}

Constraints

• Stratum must be a non-negative integer. Violations: "stratum must be a non-negative integer; got <value>".
• All verdict references must resolve to produced verdicts. Violations: "unresolved VerdictType reference: '<id>'".
• Stratum ordering: a rule at stratum N referencing a verdict from stratum N is a Pass 5 error: "stratum violation: rule at stratum N references verdict from stratum N".
• S8 -- Verdict uniqueness: no two rules may produce the same VerdictType name. Duplicate verdicts are elaboration errors.
• Variable x variable multiplication in Rule bodies requires Int-typed operands, and the product range must be contained in the declared payload type. Overflow: "type error: product range Int(...) is not contained in declared verdict payload type Int(...)".

Common Mistakes

Same-stratum verdict references. A stratum 0 rule cannot reference verdicts from another stratum 0 rule. Move the dependent rule to stratum 1.

Duplicate verdict names. Two rules producing the same verdict name fails S8. Use distinct names and compose at a higher stratum.

Variable x variable multiplication in predicates. fact_a * fact_b is forbidden in when clauses. Only fact * literal is allowed in predicates. Variable x variable is allowed only in produce clauses.

Assuming verdict re-evaluation in flows. Verdicts are frozen at flow initiation. If facts change mid-flow, verdicts are NOT recomputed. The flow uses its snapshot.

Non-deterministic logic. Rules cannot reference timestamps, random values, or ambient state. All time-varying values must enter as facts.

How Rules Connect to Other Constructs

• Facts are the sole input to stratum 0 rules.
• Operations reference verdicts in their preconditions via verdict_present(name).
• Flows use the frozen verdict set (snapshotted at initiation) for BranchStep conditions and OperationStep preconditions.
• Personas do NOT affect rule evaluation. Verdict production is persona-independent.
• Entities are NOT referenced by rules. Entity state is not a predicate term.

Static Analysis Properties

• S5 (Verdict and outcome space) enumerates all possible verdict types the contract can produce.
• S7 (Evaluation complexity bounds) computes bounds for each predicate expression tree.
• S8 (Verdict uniqueness) guarantees each verdict has a single producing rule -- enabling unambiguous provenance.
• Stratification ensures evaluation order is well-defined and terminates in finite steps.