# Procedures: states, transitions, carrier, fold

**In one sentence:** these constructs answer the question "where
the case stands now and how it got here". Take them when the case history is an
automaton: states, transitions on carrier events, transition conditions; and
the core derives where the case stands (`current_state`) from the history of
attempts.

A case history is an automaton — states, transitions on carrier events, guards — and the engine folds the attempt history into the current state.

## 1. When to take it and when not to

| Instead of | Selection rule |
|---|---|
| Procedure vs a set of `strict` rules | Case history is a sequence of states with strict order ("filing first, review after") — procedure: the order comes from carrier time, not from rule positions in the file. Independent unordered conditions — plain rules |
| `on E` vs a transition without `on` | Carrier is a domain event (filing, opening, signing) — an `on` clause with a declared event; the carrier type is checked (`LDC-E1344`, `TRANSITION_CARRIER_TYPE_MISMATCH`). A step with no domain event — a transition without `on`, carrier is a synthetic `<P>Step` with `id`/`time` |
| `entered_state(x, S, e)` vs `current_state(x, S)` | "Entered BY this event" (re-entry is a new fact with a new carrier) — `entered_state` with a carrier; "where it stands now" (projection of the end of history) — `current_state`; "starts in" — `initial_state`. The two-argument `entered_state` no longer exists |
| `when` vs `requires` | Condition on world facts — guard `when` (sees the prefix state); condition on completion of another procedure/instance — `requires completed(P, y)`. A guard reading a power effect or a rule over the fold — `LDC-E1348` |
| `parallel` with regions vs two procedures | One step — two independent motions (two tokens, one carrier) — `parallel` regions with `join`; two separate histories — two procedures. One carrier — one atomic step, otherwise `CARRIER_REUSED` |

## Grammar: event and record constructor (EBNF verbatim from the grammar)

An event declaration — fields with mandatory constructor `id`/`time` (without them — `LDC-E1343`):

```ebnf
event_decl              = "event", identifier,
                          [ ":", type_ref ], "{",
                            { field_decl | label_item | metadata_item },
                          "}" ;
```

A record constructor — the same record in `const`, case-`const`, and assertion-argument positions (executable in three positions):

```ebnf
record_literal          = qualified_name, "{",
                            [ record_field, { ",", record_field }, [ "," ] ],
                          "}" ;
record_field            = identifier, ":", expression ;
```
## 2. Minimal example

Package `research.procedure.accreditation`: an application goes `Draft → Submitted`
on the `ApplicationFiled` event when the application is complete; then —
`Accredited`.

```law
procedure Accreditation(app: Application) {
    state Draft initial;
    state Submitted;
    state Accredited terminal;
    transition Submit {
        from Draft;
        to Submitted;
        on ApplicationFiled;
        when application_complete(app);
    }
    transition Grant {
        from Submitted;
        to Accredited;
    }
}
```

Case 1: instance + `application_complete` + a `Submit` attempt with carrier
`ApplicationFiled { id, time: @2026-04-14T10:00:00+05:00 }`. Query:
`evaluate truth(current_state(app17, Submitted))`. Case 2: instance only;
query `initial_state(app17, Draft)`.

Observed engine answer (installed `law`, semantics `law.core/0.2`):

```text
law test research.procedure.accreditation: мир research.procedure.accreditation
  ok   [research.procedure.accreditation#authored] tests/01-submitted.lawtest / urn:query:research-procedure-01
  ok   [research.procedure.accreditation#authored] tests/02-no-attempt.lawtest / urn:query:research-procedure-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Case 1 answers
`TRUE_ONLY` with `COMPUTED`: the transition is valid (state before the carrier —
`from`, type matched `on`, guard true), the fold publishes
`valid_transition`, `left_state(Draft)`, `entered_state(Submitted)`.
Case 2 — `initial_state(Draft)` — `TRUE_ONLY`: history empty, the initial
state holds without a carrier. Sensitivity: removing the attempt from case 1
changes the answer from `current_state(Submitted)` to the initial state (case 2);
removing `application_complete` leaves the case in `Draft` — see the second
package.

Second package `research.procedure.chain` — same procedure, two outcomes:

| Facts | Question | Answer | Why |
|---|---|---|---|
| instance + `Submit` attempt, guard false | `current_state(Draft)` | `TRUE_ONLY` | transition invalid — the attempt stays an attempt, state unchanged |
| instance + completeness + `Submit`, then `Grant` with synthetic `AccreditationStep` | `current_state(Accredited)` | `TRUE_ONLY` | two history steps, order by carrier `time` |

## 3. Example by domain

- **Law:** RK procurement (package `kz.corpus.procurement`, Kazakhstan) — transitions `on BidsOpeningHeld` / `on
  ContractConcluded` (see `corpus-forms.md`): domain carrier events with guards.
- **Standard/protocol:** this page's examples —
  the same device in miniature (`ApplicationFiled`, synthetic
  `AccreditationStep`); the teaching package repeats it almost verbatim.
- **Sport:** FIDE chess (package `fide.laws.chess`, international sport) — synthetic carriers `GamePlayStep`:
  no domain events for moves — case steps, `entered_state` with
  carrier and `left_state` in queries.
- **Religion/custom:** the "Queue" queue — absence and roll-call events as
  attempt carriers; the neighbouring link — the duty activation formula
  `entered_state(x, Draft, e)` reads entry with a carrier,
  initial entry — predicate `initial_state(x, S)` without a carrier.

## 4. How the engine answers

Table — observed runs of this directory's examples (installed
`law`, semantics `law.core/0.2`):

| Facts | Question | Answer | Why |
|---|---|---|---|
| instance + completeness + `Submit` attempt | `current_state(Submitted)` | `TRUE_ONLY` | all four validity conditions |
| instance only | `initial_state(Draft)` | `TRUE_ONLY` | empty history, initial holds |
| instance + attempt without completeness | `current_state(Draft)` | `TRUE_ONLY` | guard false — state unchanged |
| full chain + `Grant` with synthetic carrier | `current_state(Accredited)` (plus `left_state(Draft, e_submit)` — `TRUE_ONLY`, `current_state(Draft)` — `NEITHER`) | `TRUE_ONLY` | fold of two carriers by time; left-behind and no-longer-current — from the full-chain scenario ("draft left" / "case no longer in draft") |
| instance + completeness + `Submit` attempt with an `AccreditationStep` carrier | `valid_transition(Submit, e)` | `NEITHER` + `TRANSITION_CARRIER_TYPE_MISMATCH` | carrier type mismatched `on` |

- The instance history is attempts with `supported` support at version-chain
  heads, ordered by carrier `time` start; equal starts for one instance —
  fatal `SIMULTANEOUS_EVENTS`; for different instances —
  not a refusal (a group reads the state before the group).
- An invalid transition (false guard, another instance's `from`, mismatched `on` type) —
  a routine outcome: the attempt stays an attempt, state unchanged; carrier
  type missing `on` gives `TRANSITION_CARRIER_TYPE_MISMATCH` (warning),
  a fact about another instance — `EVENT_OUTSIDE_PROCEDURE` (warning).
- A guard sees only the prefix before its carrier; reads of neighbouring
  predicates go inside the fold as prefix state; a predicate
  produced above the fold (rule over the fold, power effect,
  status atom) — `LDC-E1348` / fatal `NON_EXECUTABLE_UNSTRATIFIED`.
- Guard and `requires` — carriers of the judgment channel:
  a live transition with an open judge answers `NEITHER` with
  `REQUIRES_JUDGMENT`; a rule reading transition facts inherits judges.
- `current_state` is non-monotone (end projection), the rest is monotone over
  the prefix; one law for the whole history (`legal_time` — on the document).

## 5. Common mistakes

1. Record order in the case instead of carrier `time` — history is ordered by
   the start of canonical `time`; records are read as a set
   (`pitfalls.md`, item 1).
2. Two-argument `entered_state(x, S)` — the form no longer exists: "stands" —
   `current_state`, "starts" — `initial_state`, "entered by this" —
   `entered_state` with a carrier (`pitfalls.md`, item 2).
3. Same-name members of two procedures — a bare name resolves via the package
   member table; a duplicate — `LDC-E1351` (`pitfalls.md`, item 3).
4. Guard reading a power effect or a status — `LDC-E1348`: rewrite to
   empirics or `requires completed(P, y)` (`pitfalls.md`, item 4).
5. One carrier for two transitions of one region — fatal `CARRIER_REUSED`;
   concurrency — only in independent `parallel` regions
   (`pitfalls.md`, item 5).
6. Initial entry presented as `entered_state` — forbidden: it has
   no carrier; the activation formula does not bind it (binding it would
   fail reading `e.time`; `pitfalls.md`, item 6).

## 6. References

- Tutorials: [procedure](/tutorials/procedure/), [procedure exercise](/tutorials/exercise-procedure/);
  the process layer (frames across editions, decision journals) lives in tooling, not in the core fold.