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:

• .discussion/lessons/DSC-0007-pbs-learn-to-discussion-lessons-migration/LSN-0020-pbs-runtime-values-identity-memory-boundaries-legacy.md
• .discussion/lessons/DSC-0007-pbs-learn-to-discussion-lessons-migration/LSN-0022-pbs-globals-lifecycle-and-published-entrypoint-legacy.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.