Semantic Constraints

After parsing, the Grove checker applies a set of semantic rules that go beyond grammar. These constraints enforce the invariants required for correct state management, deterministic replay, and safe schema evolution. A program that parses successfully may still fail the checker.

Prerequisites: Declaration Grammar, Statement Grammar, Type System. What you'll learn: Every semantic rule enforced by grove check, including reserved fields, emit restrictions, for loop restrictions, validate body requirements, upcast version ordering, annotation semantics, and Value type restrictions.

Reserved Fields

The following field names are reserved by the Grove runtime and must not appear in user-defined record or event declarations:

Field	Type	Purpose
`pk`	`String`	Internal primary key (composite of module + entity id)
`id`	`Id`	Entity identifier, auto-populated from the `@create` event
`version`	`Int`	Monotonically increasing event sequence number
`created_at`	`DateTime`	Timestamp of the `@create` event
`updated_at`	`DateTime`	Timestamp of the most recent event
`created_by`	`String?`	Principal that triggered the `@create` event
`updated_by`	`String?`	Principal that triggered the most recent event

These fields are automatically managed by the runtime. They are accessible in query bodies and projections but cannot be set in emit statements.

Checker rule: If any record or event declaration defines a field whose name matches a reserved field, the checker reports an error.

Emit Restrictions

The emit statement is only permitted in specific declaration contexts:

Declaration	`emit` allowed?
`action`	Yes
`workflow`	Yes
`test`	Yes
`function`	No -- functions must be pure
`query`	No -- queries are read-only
`validate`	No -- validators check, not mutate
`activity`	No -- activities interact with external systems; emit from the calling workflow
`upcast`	No -- upcasts transform event data

Checker rule: An emit statement in a disallowed context produces the error: emit is not permitted in <declaration-kind> bodies.

Transitive Emit Prohibition

If a function calls another function, neither may contain emit. The checker verifies this transitively: a function that calls an action (which may emit) is itself a type error because actions cannot be called from functions.

For Loop Restrictions

For loops have restricted behavior to maintain determinism:

No break or continue. Grove does not have these statements. To skip an iteration, use if inside the loop body. To exit early, restructure using filter before the loop.
Mutable variable capture. A for loop may modify a mut variable declared in an enclosing scope. This is the primary mechanism for accumulation patterns:
```
let mut total = 0.0
for item in items {
  total = total + item.price * item.quantity
}
```
No nested emit in validate. Within a validate body, for loops must not contain emit statements (though emit is already prohibited in validate entirely; this rule catches indirect violations).

Checker rule: A for loop body that assigns to a non-mut variable produces: cannot assign to immutable variable '<name>'.

Validate Body Requirements

A validate block must satisfy these constraints:

Only if + fail patterns. The body of a validate must consist exclusively of if statements whose bodies contain fail statements. Let bindings for intermediate computations are also permitted.
No emit. As noted above, emit is forbidden in validate.
No return. A validate block has no return type; return is not permitted.
Scope. The fields of the event being validated are in scope as local variables within the validate body.

// Valid
validate OrderCreated {
  let item_count = items.length
  if item_count == 0 {
    fail "Order must have at least one item"
  }
  if total < 0 {
    fail "Total cannot be negative"
  }
}

// Invalid -- emit is not allowed
validate OrderCreated {
  emit AuditLog { message: "validating" }  // ERROR
}

Checker rule: A non-if/let/fail statement in a validate body produces: only if/fail/let statements are permitted in validate blocks.

Upcast Version Ordering

Upcast declarations must form a contiguous chain from the oldest version to the current version:

Sequential versions. For an event E with current version N, upcasts must exist for every pair (v, v+1) where 1 <= v < N.
No gaps. If version 3 is the current version, both upcast E:1 -> 2 and upcast E:2 -> 3 must be defined.
No duplicates. At most one upcast may exist for each (from, to) pair.
Monotonic. The to version must equal from + 1. You cannot skip versions (e.g., upcast E:1 -> 3 is invalid).

// Event at version 3 requires two upcasts:
event OrderCreated:3 {
  customer_id: Id
  items: List<OrderItem>
  total: Decimal
  currency: String       // added in v2
  source: String          // added in v3
}

upcast OrderCreated:1 -> 2 {
  let currency = "USD"
}

upcast OrderCreated:2 -> 3 {
  let source = "unknown"
}

Checker rule: A missing upcast in the chain produces: missing upcast for <EventName>:<from> -> <to>.

Checker rule: A non-sequential upcast produces: upcast target version must be exactly <from> + 1.

@create and @delete Semantics

@create

Exactly one event in a module may be annotated with @create.
The @create event initializes an entity. Before this event is emitted, the entity does not exist.
If a module defines any events, it must define exactly one @create event.
Emitting a @create event for an entity that already exists is a runtime error.

Checker rule: Zero @create events in a module with events produces: module defines events but has no @create event.

Checker rule: Multiple @create events produces: only one @create event is permitted per module.

@delete

At most one event in a module may be annotated with @delete.
The @delete event logically deletes the entity. After this event, no further events may be emitted for the entity.
@delete is optional; not all entities support deletion.
Emitting any event for a deleted entity is a runtime error.

Checker rule: Multiple @delete events produces: only one @delete event is permitted per module.

Value Type Restrictions

The Value type is a dynamic escape hatch subject to these constraints:

No direct field access. Accessing .field on a Value is a type error. Use .get("field") instead.
No arithmetic. Arithmetic operators (+, -, *, /, %) do not operate on Value. Extract a numeric type first.
No comparison except equality. == and != work on Value (deep equality). Ordering operators (<, >, <=, >=) do not.
No Map key. Map<Value, T> is a type error. Map keys must be String or Id.
Lint warning on event fields. Event fields typed as Value trigger a lint warning because they bypass schema evolution. This is a warning, not an error; it can be suppressed with a comment directive.

Checker rule: Direct member access on a Value produces: cannot access field '<name>' on Value; use .get("<name>") instead.

Checker rule: Arithmetic on Value produces: operator '<op>' is not defined for type Value.

Additional Constraints

Action Uniqueness

Within a module, action names must be unique. Two actions with the same name produce a checker error.

Event Name + Version Uniqueness

The combination of event name and version number must be unique within a module.

Function Purity

Functions may not call actions, emit events, publish messages, or perform any I/O. They may call other functions and use only pure expressions.

Checker rule: A function body that calls an action produces: cannot call action '<name>' from a function; functions must be pure.

Query Read-Only

Queries may not emit events, publish messages, or call actions. They may call functions and access projected state.

Checker rule: An emit in a query body produces: emit is not permitted in query bodies.

Workflow and Activity Separation

Workflows may call activities but activities may not call workflows. This prevents re-entrancy in the durable execution engine.

Checker rule: An activity body that calls a workflow produces: cannot call workflow '<name>' from an activity.