Commit Loops

Commit loops are the core Nilakan feature. They initialize state with init, run a while guard, stage primed next-state updates, and commit those updates together at the end of each round.

Motivation

A commit loop expresses one repeated state transition. This is useful for algorithms that are most naturally written as difference equations: each round reads the current state, computes the next state, and then commits the next state all at once.

In a loop over state x, x means the current value for this round and x' means the next value being staged. At the beginning of every round, Nilakan seeds x' from x. Explicit primed assignments override that seed. At the commit boundary, x' becomes x for the next round.

Syntax

def exchange() -> tuple[num, num]:
  init:
    left = 1
    right = 2
    done = False
  while not done:
    left' = right
    right' = left
    done' = True
  return left, right

init must be adjacent to the while it introduces. State names assigned in init may be assigned with one prime in the loop body. init assignments may also carry type annotations.

Fragment — valid only immediately before its while

init:
  i: num = 0
  seen: set[str] = set()

pragma rhs_prime: <guarantee> may appear between init and while. A bare nested while is only valid inside a commit-loop body, where it becomes another commit loop.

Sparse list and dict updates use primed subscript assignment.

def swap_first_two(xs: list[num]) -> list[num]:
  init:
    items = xs
    done = False
  while not done:
    items'[0] = items[1]
    items'[1] = items[0]
    done' = True
  return items

Semantics

Before each round, Nilakan applies the following rule to every state variable:

1. Copy the current value into the next-state layer.
2. Apply the primed writes selected by that round.
3. Commit the complete next-state layer together.

Therefore, omitting a primed write means “retain the current value.” It does not mean “clear the value,” “reset it to its initializer,” or “leave it undefined.” Sparse list and dict updates depend on this seed: items'[1] = value starts with a copy of items, replaces one position in that copy, and leaves every other position unchanged.

Temporary assignments inside a commit loop are local to the round. By default, Nilakan schedules the round with a dependency DAG over temporaries, branch guards, and staged writes.

State variables must be updated with primed assignment. Unprimed assignment to a state variable inside the loop body is rejected.

Branches in a commit loop are selected once for the round. Mutually exclusive branches may write the same primed target.

A normal guard is checked before the round. A guard containing a primed value requires a speculative round to create that next state, and a false result discards it.

Dependency Scheduling

Normal commit loops use the DAG scheduler and forbid primed right-hand-side reads. This preserves the frozen-current-state model while still allowing temporaries and branch guards to be evaluated in dependency order.

The scheduler is deterministic. Dependencies always run before their consumers. When two nodes are ready at the same time and neither depends on the other, they run in source order. Visualizations should display that same order.

if, elif, and else can appear anywhere in a loop body and can nest. Each guard must be boolean. Guards are evaluated once, in order, until one succeeds. Later guards and unselected bodies do not execute or contribute dependencies to the round.

Selecting a branch adds its statements to the active dependency graph. Those statements can run between statements from the containing block when their dependencies require it. A conditional is not an indivisible scheduling unit.

def choose(flag: bool) -> num:
  init: result = 0; done = False
  while not done:
    if flag:
      chosen = 3
    else:
      chosen = 4
    doubled = chosen * 2
    result' = doubled
    done' = True
  return result

print(choose(True))

This prints 6. Assignments in a selected branch make their temporary values available to later code in that round. An existing temporary keeps its incoming value when a branch does not replace it. A new temporary remains uninitialized on paths that do not assign it; reading it on such a path raises UndefinedVariableError. A declaration in some branch does not give the name a default value. Temporaries are recreated for every round, so a value from an earlier round cannot fill that gap.

Separate conditionals may share a temporary when their selected path initializes it before use:

def maybe_double(flag: bool) -> num:
  init: result = 0; done = False
  while not done:
    if flag:
      chosen = 3
    if flag:
      result' = chosen * 2
    done' = True
  return result

print(maybe_double(False))

This prints 0: neither branch runs, so the program never reads chosen and result retains its seeded value. DAG scheduling also allows a first use to precede its declaration in source when the selected dependencies are acyclic. Temporary reassignments preserve the values observed by earlier consumers. A later assignment in the containing block cannot replace a branch’s local value before that branch consumes it.

Dependency cycles on the executed path are errors. A dependency appearing only in an unselected branch or later, untested elif guard cannot create a cycle for the selected path.

With a non-sequential_dependent rhs_prime pragma, the same DAG scheduler also includes next-state read dependencies. Primed reads observe the next-state layer after any dependency writes that the DAG schedules first. An outside write to y' runs before a selected branch statement that consumes y'; other statements in that branch may run earlier. Current-state reads still observe the frozen current layer, including inside nested loops.

With pragma rhs_prime: sequential_dependent, Nilakan uses source-order scheduling. Primed reads observe prior primed writes in source order.

Standalone function call statements act as scheduling barriers: statements before the call stay before it, and statements after the call stay after it.

Effects And Commit

Output is part of a round’s transaction. A print(...) call records output in the active round. Nilakan publishes those records, in call order, only when the round commits. It discards them when a primed guard rejects a speculative round or when the round fails.

Nested rounds merge committed output into the containing round rather than publishing it early. If the containing round is later discarded, output from its nested loops is discarded with it. Output outside a commit loop is immediate.

rhs_prime Pragmas

pragma rhs_prime: <guarantee> allows a loop body to read primed values on the right-hand side under an explicit guarantee.

Supported guarantees are:

• monotone_convergent: updates move monotonically toward a unique fixpoint independent of update order.
• idempotent: applying the update more than once has the same result as applying it once.
• confluent: every allowed ordering of within-round updates reaches the same result.
• associative_commutative: the accumulating operation is associative and commutative, so grouping and ordering do not change the result.
• sequential_dependent: the computation intentionally depends on source order and makes no order-independence claim.

The first four names state different proof obligations, but currently select the same deterministic DAG execution policy. They are not aliases conceptually: the programmer is recording why the within-round primed reads are valid. sequential_dependent is operationally different because it selects source-order scheduling.

Execution policy:

| Surface syntax | Scheduler | Primed RHS reads | | ------------------------------------------- | ------------ | ---------------- | | no pragma | DAG | forbidden | | pragma rhs_prime: monotone_convergent | DAG | allowed | | pragma rhs_prime: idempotent | DAG | allowed | | pragma rhs_prime: confluent | DAG | allowed | | pragma rhs_prime: associative_commutative | DAG | allowed | | pragma rhs_prime: sequential_dependent | source order | allowed |

If a guard reads primed state, Nilakan runs a speculative body round before evaluating the guard. When that guard exits the loop, the final speculative next state is discarded. Errors raised while computing the speculative round are still reported. The example returns limit - 1 for a positive integer limit: when the speculative next value reaches limit, the guard becomes false and that round is discarded.

def advance_until(limit: num) -> num:
  init:
    x = 0
  pragma rhs_prime: sequential_dependent
  while x' < limit:
    x' = x + 1
  return x

State Layers And Nested Loops

Nested commit loops apply the same current/next rule one prime layer deeper.

| Context | Current | Next | | ------------------ | ------- | ------ | | outer loop | x | x' | | nested loop | x' | x'' | | third-level nested | x'' | x''' |

Statements preceding a nested loop finish before it starts. The inner loop treats the parent’s staged next-state layer as its current layer. When the inner loop commits, x'' becomes x'; when the outer loop later commits, x' becomes x.

This is why a nested loop can read x' without rhs_prime: for that nested loop, x' is current state. Reading x'' inside the nested loop is a read of the nested next-state layer and requires a nested rhs_prime pragma.

rhs_prime pragmas are scoped to the immediately following commit loop. An outer pragma does not authorize nested loop body reads of the nested next-state layer.

Constraints And Errors

Primed assignment is only legal inside a commit loop. Duplicate primed writes to the same target on the same path are rejected. Sparse primed updates are implemented for lists and dicts, not for sets or tuples.

Whole writes and sparse writes to the same state variable conflict on the same path. Duplicate literal sparse slots or keys also conflict on the same path. Mutually exclusive branches may write the same state variable. Separate conditionals may also select writes to the same target when only one of those writes executes. Conditional conflicts are checked against the selected round; an unselected write does not conflict with an executed write.

Set and tuple sparse primed updates are rejected.

A nested loop is a scheduling boundary. When it finishes, execution resumes with the remaining statements in the containing branch or loop body. Statements after that boundary may consume its committed result from the parent’s next-state layer under the usual rhs_prime rule. Output from both the nested loop and the resumed statements remains part of the enclosing round’s transaction.

Commit loops finish only when their while guard is false. break, continue, and early return are not supported in their bodies, including inside conditional branches.

Nested loops inherit parent state at the current prime depth. A nested init can create local state with unprimed spelling, and that local state does not leak after the nested loop exits. A nested init can also override inherited state at the inherited spelling, such as init: x' = x + 1 inside a loop where x' is the nested current state. New nested local state must use unprimed spelling.

The default maximum source prime depth is 5.

Examples

Sparse list update:

def swap_edges(values: list[num]) -> list[num]:
  init:
    arr = values
    step = 0
  while step < 1:
    arr'[0] = arr[2]
    arr'[2] = arr[0]
    step' = step + 1
  return arr

print(swap_edges([1, 2, 3]))

RHS-prime update:

def accumulate() -> list[num]:
  init:
    xs = [1, 2]
    step = 0
  pragma rhs_prime: idempotent
  while step < 1:
    xs'[1] = xs'[0] + 1
    xs'[0] = 11 if xs[0] < 11 else xs[0]
    step' = 1
  return xs

print(accumulate())

The update is idempotent: it clamps xs[0] to at least 11, derives xs[1] from that staged value, and sets step to 1. Applying the body again therefore leaves the committed state unchanged.

Nested rhs_prime:

def nested_next_read() -> num:
  init:
    i = 0
    total = 0
    outer = 0
  while outer < 1:
    outer' = outer + 1
    pragma rhs_prime: idempotent
    while i' < 1:
      total'' = total' + i''
      i'' = i' + 1
  return total

print(nested_next_read())

Duplicate write error shape:

Intentional failure — NLK3005

def bad() -> num:
  init:
    x = 0
  while x < 1:
    x' = 1
    x' = 2
  return x