prometeu-studio/docs/specs/compiler-languages/pbs/9. Dynamic Semantics Specification.md

# PBS Dynamic Semantics Specification

Status: Draft v1 (Temporary)  
Applies to: runtime-observable behavior of PBS core programs

## 1. Purpose

This document defines the normative dynamic semantics of PBS core.

Its purpose is to make runtime behavior convergent across implementations by fixing:

- execution ordering,
- runtime evaluation of expressions and statements,
- abrupt completion and propagation behavior,
- runtime behavior of effect surfaces such as `optional` and `result`,
- the execution boundary between ordinary PBS code, callbacks, contract calls, and host-backed calls.

## 2. Scope

This document defines:

- the observable execution model of PBS core,
- evaluation order for expressions, statements, and blocks,
- runtime branch selection for `if` and `switch`,
- runtime application behavior for `apply`, call sugar, methods, contracts, callbacks, and host-backed call surfaces,
- runtime behavior of `optional`, `result<E>`, `else`, `!`, and `handle`,
- abrupt completion (`return`, `break`, `continue`) and trap propagation,
- determinism requirements that affect execution behavior.

This document does not define:

- static typing or overload resolution rules,
- GC algorithm internals,
- exact IR shape or lowering passes,
- diagnostics catalog wording,
- the full PBX binary format.

## 3. Authority and Precedence

Normative precedence:

1. Runtime authority (`docs/specs/hardware/topics/chapter-2.md`, `chapter-3.md`, `chapter-9.md`, `chapter-12.md`, `chapter-16.md`)
2. Bytecode authority (`docs/specs/bytecode/ISA_CORE.md`)
3. `3. Core Syntax Specification.md`
4. `4. Static Semantics Specification.md`
5. This document

If a rule here conflicts with higher authority, it is invalid.

## 4. Normative Inputs

This document depends on, at minimum:

- `1. Language Charter.md`
- `3. Core Syntax Specification.md`
- `4. Static Semantics Specification.md`
- `5. Manifest, Stdlib, and SDK Resolution Specification.md`
- `6.2. Host ABI Binding and Loader Resolution Specification.md`

This document integrates the following accepted decisions:

- `docs/pbs/decisions/Dynamic Semantics - Execution Model Decision.md`
- `docs/pbs/decisions/Dynamic Semantics - Effect Surfaces Decision.md`
- `docs/pbs/decisions/Dynamic Semantics - Branch Selection Decision.md`
- `docs/pbs/decisions/Host Memory Boundary Decision.md`
- `docs/compiler/pbs/decisions/Lifecycle Markers, Program Init, and Frame Root Semantics Decision.md`
- `docs/compiler/pbs/decisions/Published Entrypoint, Synthetic Wrapper, and FRAME_RET Ownership Decision.md`

## 5. Already-Settled Inputs

The following inputs are already fixed elsewhere and must not be contradicted here:

- PBS prioritizes determinism and compatibility over ergonomics when the two conflict.
- `FRAME_SYNC`-based execution semantics remain preserved.
- No non-deterministic async execution model is part of PBS v1.
- Function application is defined on the canonical `apply` surface, with call sugar desugaring to `apply`.
- `optional T` function fallthrough yields `none`.
- `result<E>` function fallthrough is a compile-time error.
- `ok(...)` and `err(...)` are special result-flow forms rather than ordinary first-class runtime constructors.
- Lifecycle bootstrap is one-shot and fail-fast.
- `[Frame]` denotes the logical userland frame root, not the physical published entrypoint by itself.

## 6. Execution Baseline

PBS execution is single-threaded per program instance in v1.

User-visible execution is deterministic and does not expose concurrent interleaving.

User-visible sequencing is defined by:

- evaluation order,
- branch selection,
- abrupt completion,
- result propagation,
- trap propagation,
- and host-call boundaries.

VM-internal frame layout, temporary storage, and lowering steps are not observable unless they change one of the semantic effects above.

`FRAME_SYNC` is the only normative safepoint in PBS v1.

## 6.1 Lifecycle bootstrap

Executable PBS programs have a logical bootstrap sequence before ordinary frame execution.

Normative order:

1. materialize globals for each file according to dependency order,
2. execute that file's `[Init]`, if present,
3. compose those steps into one synthetic module init per module,
4. execute project init, if present,
5. then invoke the userland callable marked with `[Frame]`.

Lifecycle bootstrap is one-shot:

- no automatic retry occurs after boot failure,
- failure during module init aborts boot,
- failure during project init aborts boot.

## 6.2 Logical frame root and physical wrapper

PBS distinguishes the logical frame root from the physical published entrypoint:

- the userland callable marked with `[Frame]` is the logical frame root,
- the compiler-published synthetic wrapper is the physical executable root,
- the wrapper owns final `FRAME_RET`,
- and the wrapper invokes the logical frame root after bootstrap is complete.

Nominal manifest metadata does not participate in this runtime boot choice.

## 7. Evaluation Order and Single Evaluation

### 7.1 Default rule

The default evaluation rule is strict left-to-right unless a construct explicitly states otherwise.

### 7.2 Call evaluation

For application:

1. form the call target,
2. evaluate any receiver or callable artifact needed for target formation exactly once,
3. evaluate arguments in source order from left to right,
4. invoke the resolved target,
5. produce one of:
   - normal return,
   - explicit `result<E>` propagation,
   - or `trap`.

This rule applies to canonical `apply` and to direct-call sugar that desugars to `apply`.

`apply` chains are parsed right-associatively, but their observable evaluation still follows the left-to-right rule above.

### 7.3 Exactly-once guarantees

The following expressions are evaluated exactly once where they appear:

- `if` condition,
- `switch` selector,
- the left operand of `opt else fallback`,
- the payload expression of `some(expr)`,
- the operand of `expr!`,
- the operand of `handle expr { ... }`,
- the context expression of `bind(context, fn_name)`,
- call receivers, callees, and argument expressions as required by the call rule above.

## 8. Blocks and Abrupt Completion

Statements in a block execute in source order.

Only the final unsemicoloned expression in a block contributes to the block result.

Abrupt completion terminates the current construct immediately and prevents later sibling evaluation.

At minimum, the following are abrupt-completion forms:

- `return`,
- `break`,
- `continue`,
- `!` on an error path,
- `trap`.

## 9. `optional`

### 9.1 Runtime model

`optional` has exactly two runtime states:

- `some(payload)`
- `none`

`none` is the canonical absence of payload.

### 9.2 Construction

`some(expr)` evaluates `expr` eagerly and exactly once before forming the `some(payload)` carrier.

### 9.3 Extraction

`opt else fallback`:

1. evaluates the left operand exactly once,
2. yields the extracted payload if that operand evaluates to `some(payload)`,
3. otherwise evaluates `fallback` and yields its value.

`else` is extraction with fallback, not error handling.

### 9.4 Trap behavior

`optional` is trap-free by itself.

Any trap associated with `some(expr)` or `opt else fallback` arises only from evaluating the relevant subexpressions.

## 10. `result<E>`

### 10.1 Runtime role

`result<E>` is the runtime carrier for success-or-modeled-failure at function boundaries and in expressions whose static type is `result<E> P`.

Expected, recoverable failures belong to `result<E>`, not to `trap`.

### 10.2 `!`

`expr!`:

1. evaluates `expr` exactly once,
2. yields the extracted success payload if `expr` succeeds,
3. performs immediate enclosing-function return with the same `err(...)` if `expr` yields error.

`!` does not:

- remap errors,
- intercept traps,
- or continue ordinary evaluation after the propagated error path is chosen.

### 10.3 `handle`

`handle expr { ... }`:

1. evaluates `expr` exactly once,
2. yields the extracted success payload directly if `expr` succeeds,
3. selects exactly one matching arm if `expr` yields error,
4. executes that arm,
5. requires the arm to terminate with either `ok(payload)` or `err(E2.case)`.

`ok(payload)` in a `handle` arm recovers locally and makes the `handle` expression yield `payload`.

`err(E2.case)` in a `handle` arm performs immediate enclosing-function return with `err(E2.case)`.

For the remap-only case, a short form such as `E1.case -> E2.case` is sugar for an arm block that returns `err(E2.case)`.

`handle` may execute user-defined logic inside an arm, but it remains specific to modeled `result` errors.

`handle` does not intercept or convert traps.

## 11. `apply`, Call Sugar, and `bind`

### 11.1 Canonical role of `apply`

`apply` is the canonical universal call surface in PBS v1.

The same observable call model applies to:

- top-level functions,
- struct methods,
- service methods,
- contract calls,
- callback calls,
- host-backed calls.

Callable-specific dispatch may differ internally, but it does not change the user-visible sequencing model defined in this document.

### 11.2 Effect boundaries

`apply` does not introduce implicit effect composition.

If a callable returns:

- `optional<P>`, extraction remains explicit through `else`,
- `result<E> P`, propagation or processing remains explicit through `!` or `handle`.

### 11.3 `bind`

`bind(context, fn_name)` is the explicit callback-formation mechanism in PBS v1.

It:

- evaluates `context` exactly once,
- captures the same struct context identity without copying it,
- attaches that context to the resolved top-level function target,
- produces a callback value whose invocation behaves as if the target function were called with the captured context as its first argument.

At the language-semantics level, `bind` is trap-free.

Incompatible binding shape remains a compile-time matter rather than a runtime failure mode.

Retention and storage consequences of `bind` belong to `Memory and Lifetime Specification.md`.

## 12. Branch Selection

### 12.1 `if`

`if` evaluates its condition exactly once.

If the condition is `true`, only the selected `then` branch executes.
If the condition is `false`, only the selected `else` branch executes.

The non-selected branch is not evaluated, even partially.

### 12.2 `switch`

`switch` evaluates its selector exactly once and executes exactly one selected arm.

The non-selected arms are not evaluated.

`switch` is restricted to statically discriminable selector categories in v1:

- literal-comparable scalar values,
- enum values,
- canonical `str` values,
- and any other selector category admitted elsewhere by explicit specification.

`switch` does not accept:

- `result`,
- `error`,
- structs,
- string object/reference types distinct from canonical `str`,
- heap-backed selector categories.

Matching is exact and deterministic:

- enum selectors match by canonical enum-case identity,
- scalar selectors match by the exact equality rule for that scalar category,
- `str` selectors match by canonical static string identity.

`switch` does not perform structural matching, guard evaluation, or user-defined equality dispatch.

## 13. Trap, Determinism, and Host Interaction

### 13.1 Trap boundary

`trap` is reserved for failures that are:

- outside the ordinary userland contract,
- not suitably representable as the declared `result<E>` surface,
- caused by runtime or host invariant failure,
- or severe enough that ordinary userland recovery is not part of the v1 language model.

PBS v1 does not define `try/catch` for traps.

Traps are not part of ordinary recoverable control flow.

Any trap aborts the current PBS program execution rather than returning control to ordinary userland flow.

Control then transfers to runtime or firmware crash handling outside the ordinary language model.

### 13.2 Host interaction

Host calls must not introduce user-visible reordering of already-defined PBS evaluation order.

Expected operational failures of host-backed surfaces should be modeled through their declared contract rather than through ad hoc trap usage.

Cross-boundary host/userland interaction remains stack-value-based as defined by the host-boundary decision track; direct host-memory manipulation is not part of PBS userland semantics.

## 14. TODO

The following items remain editorial or cross-spec integration tasks rather than open semantic agenda questions:

- the final wording split between this document and `16. Runtime Execution and Initialization Specification.md` for crash handoff after trap,
- the final wording split between this document and `10. Memory and Lifetime Specification.md` for retention/allocation facts that arise during ordinary execution,
- conformance-oriented example coverage once `13. Conformance Test Specification.md` is expanded.

## 15. Non-Goals

- Reopening grammar or static typing unless current text is impossible to execute normatively.
- Defining exact GC collection strategy.
- Designing future async, actor, or scheduler models.
- Specifying backend optimization policy.

## 16. Exit Criteria

This document is ready to move beyond temporary draft status only when:

1. every runtime-observable core construct has deterministic evaluation wording,
2. trap versus status-value behavior is explicit for every effect-bearing construct,
3. host-call interaction rules are stated without relying on informal prose elsewhere,
4. the document can drive runtime conformance tests without decision backfill,
5. the remaining TODO items are reduced to editorial integration rather than semantic uncertainty.