Specification · v1

Executable subset

A contract that parses is not yet a contract that runs. To be valid it must stay inside the executable subset below. Each rule names the diagnostic kind[code] that enforces it. The order in which they are checked is in Validation.

1. Mode

ENFORCEMENT_MODE: enforced is required (semantic[enforcement-mode]). A contract without a mode is refused the same way.

advisory and audit, in lower or upper case, parse. ulang-lite refuses them unless the caller turns the requirement off (requireEnforced: false). The mode never changes a decision: evaluation is the same in every mode.

2. CONTEXT: one entity, and its constants

• CONTEXT is required (semantic[context-required]).
• It holds exactly one ENTITIES block, and the block is named (semantic[entity]). That name is the contract's facts entity.
• Every field has a primitive type: int, float, bool or string (unsupported[type-unsupported]). Field names are unique (semantic[fields]).
• There is at most one CONSTANTS block, and it is anonymous (unsupported[constants-named]).

2.1 Constants

Every constant is:

bool and string constants are not executable. Write those values as literals in the condition.

Constants are not facts. They are named numbers that conditions compare facts against.

CONTRACT Thermostat {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Reading {
      celsius: float
      sensor_ok: bool
    }
    CONSTANTS {
      floor_c: float == -40.0 [SOURCE:SPEC-7]
      ceiling_c: float == 1.2e2 [SOURCE:SPEC-7]
    }
  }
  TRIGGER {
    accept_reading()
  }
  GUARANTEE {
    ENSURE accept_reading() WHEN Reading.sensor_ok == true [SOURCE:sensor_healthy]
  }
  PROHIBITION {
    FORBID accept_reading WHEN Reading.celsius < floor_c OR Reading.celsius > ceiling_c [SOURCE:out_of_range]
  }
}

3. TRIGGER and clauses

• TRIGGER is required (semantic[trigger-required]). It lists each governed action once, as action(): parentheses, no parameters, no WHEN guard (unsupported[trigger-form], unsupported[trigger-params], semantic[trigger-entry]).
• A guarantee clause is exactly ENSURE action() WHEN condition [SOURCE:id] (unsupported[ensure-form]).
• A prohibition clause is FORBID action WHEN condition [SOURCE:id]. FORBID action() means the same (unsupported[forbid-form]).
• A GUARANTEE block is not empty (semantic[empty-guarantee]). An empty or missing PROHIBITION is allowed.
• A clause's action must be listed in TRIGGER, and its source id must be [A-Za-z0-9_]{1,80}, written as exactly [SOURCE: (no space after [) and unique within the contract, across ENSURE and FORBID (semantic[clause-id]).
• Every action in TRIGGER has at least one clause (semantic[ungoverned-action]). An action with no rule cannot be listed.

The source id is the clause id. Decisions name clauses as <Contract>.<id>, so ids are stable public names: renaming one changes what every decision that cites it says.

4. Conditions

A condition is an AND/OR tree of typed comparisons.

Operands are literals, constant names, and Entity.field paths on the contract's own entity:

Comparisons must type-check:

Anything else is unsupported[kind-mismatch], or unsupported[nonnumeric-comparison] for strings and booleans in another shape. constant op literal (zero == 0) is unsupported[literal-comparison]: a constant is not a fact, and comparing it with a literal decides nothing.

A condition must be a comparison. A bare operand (WHEN Request.ready) or an assignment (WHEN Request.ready = true) is unsupported[condition-form]. Write Request.ready == true.

NOT, +, *, / and ^ never reach validation: the bounds scan refuses them (see Syntax §7).

The condition tree may be at most 16 levels deep by default, counting each comparison as a level (limit[condition-depth]). Parentheses add no depth. Because AND and OR associate to the left, a flat chain c₁ AND c₂ AND … AND cₙ is n levels deep: 16 comparisons with 15 operators is the longest flat chain allowed.

CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
  }
  PROHIBITION {
    FORBID grant WHEN Request.count != 0 AND Request.count != 1 AND Request.count != 2 AND Request.count != 3 AND Request.count != 4 AND Request.count != 5 AND Request.count != 6 AND Request.count != 7 AND Request.count != 8 AND Request.count != 9 AND Request.count != 10 AND Request.count != 11 AND Request.count != 12 AND Request.count != 13 AND Request.count != 14 AND Request.count != 15 [SOURCE:long_chain]
  }
}

CONTRACT Claim {
  ENFORCEMENT_MODE: enforced
  CONTEXT {
    ENTITIES Request {
      count: int
      region: string
      ready: bool
      ratio: float
    }
    CONSTANTS {
      zero: int == 0 [SOURCE:POLICY]
      cap: int == 25 [SOURCE:POLICY]
    }
  }
  TRIGGER {
    grant()
  }
  GUARANTEE {
    ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
  }
  PROHIBITION {
    FORBID grant WHEN Request.count != 0 AND Request.count != 1 AND Request.count != 2 AND Request.count != 3 AND Request.count != 4 AND Request.count != 5 AND Request.count != 6 AND Request.count != 7 AND Request.count != 8 AND Request.count != 9 AND Request.count != 10 AND Request.count != 11 AND Request.count != 12 AND Request.count != 13 AND Request.count != 14 AND Request.count != 15 AND Request.count != 16 [SOURCE:long_chain]
  }
}

5. The exact numeric domain

Every literal stays inside the range where every JSON implementation represents numbers exactly:

Integer constants are narrower still: 0 … 2^53-1. Integer literals in conditions may be negative.

6. What the subset buys

A contract inside the subset is a finite list of comparisons over one record of typed facts. It cannot loop, call out, allocate or depend on anything except the facts, so a decision always terminates, in time linear in the contract's size. That is the point of the subset: it is the part of µLang that can sit in an execution path where every effect needs a permit.