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

OverviewBoundariesCorpus formsPitfalls

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.