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.

OverviewBoundariesCorpus formsPitfalls

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)

Show syntax reference

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

Grammar

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):

Grammar

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.

Arxo 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):

Output

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, procedure exercise; the process layer (frames across editions, decision journals) lives in tooling, not in the core fold.