6 (continued). Dynamic semantics: steps, loops and concurrency

For event e = (Eₗ, v):

1. For each region Rᵢ in declaration order, take the steps step Rᵢ on p if g in source order whose pattern p matches e and whose guard g evaluates to true in (Rᵢ's pre-state fields, bindings of p). The first such step is the step of Rᵢ for e. If there is none, Rᵢ is unchanged (frame). A guard that traps (overflow, division by zero, …) does not fall through to the next step: the event is refused with that trap (change S1; this is what makes δ a total function rather than leaving the case undefined).
2. Every selected step runs on the pre-state s (ASM semantics, Form law 2): no step sees another region's update for the same event.
3. The body of the step of Rᵢ is evaluated with fields of Rᵢ bound as vars to rᵢ, the pattern bindings as lets. Its result is
   • ok(σ′): rᵢ′ = the field values in σ′ (each checked against its type range and VALUE_LIMIT), outputs oᵢ = the values emitted, in order;
   • fail(X, w) or trap(m): the step is refused.
4. If any selected step is refused, the whole event is refused: δ(s, e) = (s, [Refused(X or trap(m), e)]), where X is the refusal of the first refused region in declaration order. Atomicity: an event either applies to every region or to none.
5. Otherwise δ(s, e) = ((r₁′, …, rₖ′), o₁ ++ … ++ oₖ).

The arrow form step R on p -> e is sugar for the block f = e where f is R's only field.

Order independence. Since each step reads only its own region and the event, the result of steps 2–5 does not depend on the order regions are evaluated except through "first refused region", which is fixed by declaration order. Outputs are concatenated in declaration order.

A fail X(…) or a trap inside a step refuses the event: the state is unchanged, the log records the event with outcome refused(X) and λ outputs Refused. Nothing is thrown past a step; no event is dropped silently. In a pure function called from comptime, refusal is a compile error. In main, a trap or unhandled failure ends the command with the refusal as its output.

Channel ids, actor ids and task ids are not counters. Each is the SHA-256 of the canonical JSON of (creating construct's name-free key, creating task id, per-task creation index), where the name-free key replaces identifiers by their De Bruijn position (Form law 2). Renaming every identifier in a program therefore leaves every id, every log hash and every select decision unchanged (T7).

for p in e iterates over a finite value (list, set, map in canonical order, text by scalar value, or an integer range a..b / a..=b); its length is fixed when the loop starts, and mutating the iterated collection inside the loop is refused statically (it is borrowed). while c bound n and loop bound n run at most n iterations, n a comptime-or-runtime u64 evaluated once; the default bound is LOOP_LIMIT = 1,000,000. A program may set its own default with a module-level const LOOP_LIMIT: u64 = n, n a positive literal (draft 0.5; any other declaration of that name is refused, W-LOOP-1). Starting iteration n + 1 is trap("loop bound"). Comptime evaluation uses the same bounds. for x in f(…) over an iterator function (5.14) counts yields against LOOP_LIMIT in the same way; Lean: RCE/Iter.lean (drive_total, drive_break).

Structural recursion (draft 0.4). A function may call itself when every self-call passes, in one parameter position i fixed for the function, a name bound inside a constructor pattern of a match whose scrutinee is parameter i (or a name already known to be such a component). The argument is then a strict component of the value received, so along any chain of calls the value at position i strictly shrinks and the depth of recursion is at most the number of constructor nodes in that value, which N9 bounds. A name that is rebound by let, var, assignment or a for pattern loses this status. The checkers of drafts 0.4 to 0.7 let the position differ from call to call; that admits a function that never returns (f(x, y) whose one self-call takes a component of x and a fixed value for y, and whose other takes a fixed value for x and a component of y, runs forever from f(Leaf, Node(…))), so such a function is refused (W-REC-1; an erratum, C.15). Every function this paragraph admits is admitted by the rule below with one layer.

Recursion by layered measures. Every cycle of the call graph (a strongly connected component: one function that calls itself, or two or more functions; trait methods excluded) is admitted when its calls can be done in layers. A layer gives each function f of the cycle a set P f of parameter positions and the summed measure μ_f(ā) = Σ_{i ∈ P f} size(aᵢ), with size the number of constructor nodes. A call g(b̄) written in f keeps the measure when the positions P g map one to one into P f so that the argument at each j ∈ P g is the parameter at its image i (unchanged, the name not rebound) or a component of it in the sense of structural recursion above; it shrinks the measure when at least one of them is a component. Layer 1 must be kept by every call of the cycle and shrunk by at least one; the calls it shrinks are done. Layer 2 must be kept by every call not yet done and shrunk by at least one of them, and so on. The cycle is admitted when the calls left after some layer k form no cycle among the functions. Then the tuple (μ₁, …, μ_k, rank of the function) falls lexicographically at every call: a call done at layer j keeps μ₁ … μ_{j−1} and shrinks μ_j, and a call left over keeps every μ and lowers the rank. The order is well founded, so every chain of calls is finite; with one layer a chain inside the cycle has at most (μ + 1)·k calls, with μ the measure of the first call and k the number of functions in the cycle, and N9 bounds μ. The reference checker tries every choice of the sets of a layer, in a fixed order, for a cycle with at most 16 parameters in total, takes the first choice that does the most calls, and refuses a larger cycle that needs a layer. Lean: RCE/Mutual.lean (call_dec, call_keep, layer_dec, wf_total, wf_fuel_irrelevant; one layer: lex_dec, mutual_total, mutual_fuel_irrelevant, mutual_depth). Examples: even(xs) and odd(xs) that each call the other on the tail of a matched Cons (one layer); h(m, n) that calls h(m', n) and h(m, n') on components m' of m and n' of n (layer {m} does the first call, layer {n} the second).

Declared bounds. fn f(…) -> τ bound n, n a positive integer literal, allows at most n active calls of f at once: a call of f, once its arguments are evaluated and fitted to the parameter types, traps with trap("recursion bound") when n calls of f are already active, and otherwise counts as active until it returns or fails. A cycle that no layers admit is admitted when every cycle of calls inside it passes through a function declared with bound (the calls between functions without one form no cycle). Then the slack Σ (n_g − active calls of g) over the bounded functions falls at every call of a bounded function and the rank falls at every other call, so every run of the cycle ends, by its value or by the trap, within (slack + 1)·k nested calls. This covers recursion on integers or indices, which has no constructor measure (gcd(a, b) calling gcd(b, a % b), a parser that recurses on a position). The counts belong to the task (6.8) that makes the calls, so par and for … par inside a function of a cycle with a bounded function are refused (W-REC-1): the branches could otherwise count calls differently on one thread and on several. bound on an iterator function (5.14), a foreign function or a trait signature is W-REC-1. The check costs nothing (C.6.4 is unchanged). Lean: RCE/Mutual.lean (bump_slack, bound_dec, with lex_dec, mutual_total, mutual_depth); tests: spec/checker/tests/bound.rs.

Any other cycle in the call graph is refused (W-REC-1).

This is what makes δ total (T2): every construct terminates in a number of steps bounded by a function of the program and the event.

Concurrency is defined by a small-step semantics over configurations C = (T, K, A, L): a finite map T of tasks (id ↦ continuation), channels K (id ↦ capacity, FIFO buffer, closed flag, held-send queue), actors A (id ↦ region state, mailbox), and the log L.

Scheduling is a tick: tasks are ordered by id (6.6) and each runnable task takes exactly one communication step: it runs pure code until its next channel operation, spawn, select, emit or termination, and then performs that operation. All operations of a tick are staged and delivered after every task has moved (Form law 2: every update reads the pre-state). A tick is logged as Tick{n} plus one entry per communication action, with payloads (Form law 4).

  c has space                     ─→ v appended to c.buffer; task continues
  c full                          ─→ (c, v) held in c.held in arrival order;
                                     task blocked; Backpressure logged (no drop, law 3)
  <- c, buffer nonempty           ─→ first value; held send released in order
  <- c, empty and closed          ─→ none
  <- c, empty and open            ─→ task blocked
  spawn f(ā)                      ─→ new task id h(…); args moved in
  select: ready arms R ≠ ∅        ─→ execution k of this select statement in
                                     this task scans the arms cyclically from
                                     arm k mod n (n arms, source order) and
                                     takes the first ready one (draft 0.5)
  select: R = ∅, default present  ─→ default arm
  select: R = ∅, `after n`        ─→ blocked; after n ticks with R still ∅, after-arm

An actor is a region with a mailbox; a <- M(v) is an event M(v) admitted to a's region at the next tick; the actor runs its handlers by 6.4 with its own region as S. Each actor processes at most one message per tick, in mailbox order.

Fairness (draft 0.5). The counter k is per task and per select statement, starts at 0 and grows by one per execution. An arm that is ready at each of n consecutive executions of its select is taken by one of them (bounded wait). Draft 0.4 always took the minimal arm, so a busy first channel could starve the others, the problem Go solves with a random choice; the rotation gives the same guarantee without randomness. Lean: RCE/Select.lean (select_bounded_wait).

Because the order of every choice is a function of ids, payloads and per-select counters, and ids are content hashes, the entire run of a program is a function of its inputs: replaying the log reproduces it (T1, T3). The host may run tasks in parallel provided the observable result equals the tick semantics.

Deadlock: a tick in which no task can move and no input is pending ends the run with outcome Deadlock in λ (a defined outcome, not a hang).

example ē -> o denotes the proposition: folding the events ē from s₀ gives a final step whose outcome is o, where for -> refused: X the last event is refused with X (earlier events must be applied), and for -> e the event list is fully applied and then

• if the program has exactly one region with exactly one field f, the value of f equals ⟦e⟧;
• otherwise e must be a bool expression over the final state, with fields in scope by name (or R.f when ambiguous), and must be true.

check e (in an intent or at comptime) is the proposition ⟦e⟧ = true, evaluated at comptime. A program is admitted only if every example and check holds (W-INT-1): the gate is part of the language, not of a test harness.