# Procedures: boundaries

What the construct does NOT do: limits, reserved values, neighbouring constructs and the selection rule.

## Does not do

- **Not mutate state.** `Procedure state` is not mutated: a transition
  creates an `EnteredState` event, `current_state` is computed from history.
  Anyone waiting for a cell with assignment mistakes the model.
- **Not execute `law.procedure` as part of the minimal semantics.**
  The profile is a companion: fully lowered into events,
  institutional relations and rules.
- **Not read another history's total.** An inter-procedure guard sees
  another instance's state before `time(e_k)` (strict prefix), not
  the total: "completed" does not become true retroactively.
- **Not tell "did not happen" from "was not computed" inside the fold.**
  Hence order refusals (`SIMULTANEOUS_EVENTS`, `CARRIER_REUSED`) are
  loud fatal on the document, not local: the consumer via
  `not_known(valid_transition(...))` must tell the outcomes apart.
- **Not execute a guard on an uncomputed conclusion.** A rule is not carried
  down; executing a guard on the uncomputed means answering about the law over
  an empty relation (fatal instead of an answer).
- **Not change the law along history.** One document — one edition;
  `programHash` is a function of the program, not of history.

## Reserved and closed

- A member name is bare, unique within the package (`LDC-E1351`); a member's
  StableId is `<P>/<Name>`.
- `on` — only a declared event or action, otherwise `LDC-E1344`; a
  non-event constructor in carrier position — `LDC-E1347`; an event constructor
  requires `id`/`time` and all undeclared fields (`LDC-E1343`).
- `join` — `all`/`any`/`quorum(n)`/predicate; `quorum(n)` outside `1..m`,
  `join` without regions, a region without `initial`/terminal — `LDC-E1345`.
- `completed(P)` without an instance name — `LDC-E1349`.
- `initial` — one per automaton/region; `from`/`to` — onto declared
  states; no transition out of `terminal` (`LDC-E1311`–`E1313`).

## Neighbours and the selection rule

- Procedure vs rules: state order — procedure; independent
  conditions — rules. See the selection table in `README.md`.
- `on E` vs no `on`: domain event vs business step (synthetic
  `<P>Step`). The clause narrows, it does not introduce a carrier requirement.
- `when` vs `requires`: world facts vs procedure completion.
- `entered_state` vs `current_state` vs `initial_state`: entry by this /
  end projection / start without a carrier.
- Fold vs norm phase: the fold is one stratum below norm formation;
  power effects and status atoms are entirely above. The defeasible layer
  is split by L1 groups, not wholesale.
- Process layer vs core: frames across editions,
  decision journals — tooling; the core fold is in one edition.
- Procedure state vs norm stage ([stage](/constructs/stage/)): a state is an instance position
  in the case automaton (`current_state`); a stage is a phase of a
  norm's life, a neighbouring construct, not a case predicate.