# Procedures: pitfalls

Wrong forms, silent outcomes, `LDC-E` diagnostics, typical mistakes of
formalizers and AI agents, how to detect them. Items marked "confirmed by
run" were reproduced during this research on the installed `law`
(semantics `law.core/0.2`).

## 1. Record order instead of carrier time

History is ordered by the start of canonical `time(e)`, not by
assertion order in the case. A case recording a later event earlier
gets a time-ordered fold — the "state before `e_k`" counts from
strictly earlier events. Detection: spread carrier `time` values
meaningfully in tests; equal starts for one instance — fatal
`SIMULTANEOUS_EVENTS` (hidden order is forbidden: neither file position nor
assertion number is an order).

## 2. Two-argument `entered_state(x, S)` (confirmed by run)

The "case is in S" form no longer exists: "stands now" — `current_state(x, S)`,
"starts in S" — `initial_state(x, S)`, "entered by this event" —
`entered_state(x, S, e)`. Re-entry is a new fact with a new carrier,
not "already entered". Detection: the member name in the case is bare (`Submit`), resolved against
the presented program.

## 3. Same-name members — `LDC-E1351`

A member name (state, transition, region) is unique within the package:
one namespace for all procedures and all member kinds. A second
declaration is a static refusal `LDC-E1351` at the second in source order;
there is no qualified member spelling on the surface — the names
themselves differ (procedure prefix: `AuctionAnnounced`, `TenderAnnounced`).
Stable ids `<P>/<Name>` are distinct regardless — the ban is about
the surface. Detection: `check` on a package with two procedures.

## 4. Guard above the fold — `LDC-E1348`

A guard reading a predicate produced above the fold (rule over the fold,
power effect, status atom) is rejected statically
(`LDC-E1348`); on hand-written CLIR — fatal `NON_EXECUTABLE_UNSTRATIFIED` before
execution. Reads in head terms, aggregates, quantifiers, comparisons, `scope`
count as reads too. Detection: rewrite to empirical facts
or `requires completed(P, y)`.

## 5. One carrier — two transitions (`CARRIER_REUSED`, fatal)

Two attempts on one event are allowed only in pairwise independent regions
of one `parallel` (different regions, no ancestor relations, disjoint
write regions). Otherwise — `CARRIER_REUSED`, and the fold DOES NOT EXECUTE: no
result has `COMPUTED`. Counterexample: `Submit` and
`Withdraw` from `Draft` on one `e` — the state after `e` is not a function.
Detection: repeated support of the same ground fact is the same triple, not a new
attempt, and raises no refusal.

## 6. Initial entry as `entered_state` with a carrier

Initial entry has no carrier: it follows from
`procedure_instance(x)`; the predicate is two-argument `initial_state(x, S)`.
The activation formula `entered_state(x, Draft, e)` does NOT bind it:
a synthetic sentinel without `time` would crash the window `[e.time.start, …]`
with a refusal. "Passed through S" is written as the disjunction
`initial_state(x, S) or entered_state(x, S, _)` — the SPEC itself names
the price of two predicates.

## 7. Case `legal_time` does not cut off carriers

`legal_time` is one for the whole history: the law does not change along it, the
fold executes entirely in the chosen edition. An attempt with a carrier earlier
than `legal_time` is still an attempt. Frames across editions are tooling,
not core: the core fold runs in one edition. Detection: do not date
carriers "before the law" hoping to cut them off.

## 9. Constructor, carrier, and join diagnostics

- An event constructor without `id`/`time`, or a declared field without
  `Option`, or an undeclared field — `LDC-E1343`.
- `on` refers to something other than a declared event or action — `LDC-E1344`.
- An illegal join (`quorum(n)` outside `1..m`, `join` without regions, a
  region without `initial`/terminal) — `LDC-E1345`.
- A non-event constructor in carrier position — `LDC-E1347`.
- `completed(P)` without an instance name — `LDC-E1349`.
- A single `initial`, `from`/`to` references to declared states, no
  transition out of `terminal` — `LDC-E1311`–`LDC-E1313`.

## 8. Words after "bearer" — lowercase only

Write `bearer` only as a lowercase keyword.