diff --git a/docs/agendas/Host ABI Gate Validation Agenda.md b/docs/agendas/Host ABI Gate Validation Agenda.md
index 6a7e636f..66262e98 100644
--- a/docs/agendas/Host ABI Gate Validation Agenda.md	
+++ b/docs/agendas/Host ABI Gate Validation Agenda.md	
@@ -5,7 +5,7 @@ Purpose: validate whether the current Host ABI contract is already stable enough
 
 ## 1. Context
 
-This agenda validates whether `6. Host ABI Binding and Loader Resolution Specification.md` is already sufficient as the working contract for the path:
+This agenda validates whether `6.2. Host ABI Binding and Loader Resolution Specification.md` is already sufficient as the working contract for the path:
 
 `declare host` -> PBX metadata -> loader resolution -> numeric syscall execution
 
@@ -58,6 +58,6 @@ That means:
 
 ## 6. References
 
-- `6. Host ABI Binding and Loader Resolution Specification.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
 - `7. Cartridge Manifest and Runtime Capabilities Specification.md`
 - `8. Stdlib Environment Packaging and Loading Specification.md`
diff --git a/docs/agendas/PBS Intrinsics and Builtin Types Agenda.md b/docs/agendas/PBS Intrinsics and Builtin Types Agenda.md
new file mode 100644
index 00000000..2301af9f
--- /dev/null
+++ b/docs/agendas/PBS Intrinsics and Builtin Types Agenda.md	
@@ -0,0 +1,524 @@
+# PBS Intrinsics and Builtin Types
+
+Status: draft
+
+This document defines a proposed intrinsic model for PBS and the Prometeu VM.
+Its goal is to let the frontend expose builtin types such as `color`, `vec2`,
+and `pixel` as first-class language entities while keeping their behavior
+implemented canonically inside the VM.
+
+The design intentionally avoids coupling builtin types to the HAL. Host-backed
+behavior continues to flow through syscalls. Builtin domain behavior flows
+through VM intrinsics.
+
+## 1. Objectives
+
+This model exists to satisfy these constraints:
+
+1. Builtin types must be real language types, not just naming conventions.
+2. Builtin values must remain stack-only unless explicitly specified otherwise.
+3. Domain behavior of builtin types must execute in the VM, not in frontend-
+   generated helper code, so semantics remain canonical.
+4. Host integration must stay separate from builtin semantics.
+5. The verifier must be able to validate intrinsic calls using slot layouts.
+6. The model must scale from scalar builtins such as `color` to fixed-layout
+   aggregates such as `vec2` and `pixel`.
+
+## 2. Non-Objectives
+
+This document does not define:
+
+1. Final parser syntax for every frontend language.
+2. The full bytecode encoding that will ship in the first implementation.
+3. Heap-backed builtin types.
+4. User-extensible intrinsics.
+
+## 3. Terms
+
+### 3.1 Builtin type
+
+A builtin type is a language-level type whose semantic identity is owned by the
+runtime platform rather than by user code.
+
+Examples:
+
+- `color`
+- `vec2`
+- `pixel`
+
+### 3.2 Physical slot layout
+
+Each builtin type has a canonical physical representation in VM slots.
+
+Examples:
+
+- `color` -> 1 slot
+- `vec2` -> 2 slots
+- `pixel` -> 3 slots
+
+### 3.3 Intrinsic
+
+An intrinsic is a VM-owned operation with a canonical semantic definition.
+
+An intrinsic is not:
+
+- a user function
+- a syscall
+- a host callback
+
+An intrinsic is callable, but it is executed entirely by the VM.
+
+## 4. Three Kinds of Calls
+
+The execution model should distinguish three categories:
+
+### 4.1 Function call
+
+Calls user-defined code.
+
+- Owned by the program
+- Compiled from source bodies
+- Executed through normal `CALL`
+
+### 4.2 Intrinsic call
+
+Calls VM-defined builtin behavior.
+
+- Owned by the VM
+- Declared in the frontend as builtin members or builtin operations
+- Executed through an intrinsic dispatch path
+
+### 4.3 Syscall
+
+Calls host-managed services.
+
+- Owned by the host platform
+- Resolved by canonical identity and capability checks
+- Executed through `SYSCALL`
+
+The rule is simple:
+
+- builtin semantics -> intrinsic
+- host/platform behavior -> syscall
+
+## 5. Builtin Types Are Values, Not Just Method Bags
+
+A builtin type must define more than methods. It must define its value model.
+
+Each builtin type should specify:
+
+1. Semantic identity
+2. Physical slot layout
+3. Named fields or projections
+4. Construction rules
+5. Constants, if any
+6. Intrinsic operations
+
+### 5.1 Example: `color`
+
+`color` is a scalar builtin type.
+
+- Semantic meaning: RGB565 color
+- Physical layout: 1 slot
+- Domain behavior: conversions, comparisons, construction helpers
+
+Illustrative shape:
+
+```text
+builtin type color {
+  layout: [color]
+
+  static fn from_raw(raw: int) -> color
+  static fn rgb(r: int, g: int, b: int) -> color
+}
+```
+
+The physical carrier for a scalar builtin may be:
+
+- a dedicated `Value` variant such as `Value::Color(u16)`, or
+- another canonical 1-slot carrier defined by the VM ABI
+
+The semantic type remains `color` either way.
+
+### 5.2 Example: `vec2`
+
+`vec2` is a fixed-layout aggregate builtin type.
+
+- Semantic meaning: 2D vector
+- Physical layout: 2 slots
+- Field projections: `x`, `y`
+- Domain behavior: `dot`, `length`, `distance`
+
+Illustrative shape:
+
+```text
+builtin type vec2 {
+  layout: [float, float]
+
+  field x: float @slot(0)
+  field y: float @slot(1)
+
+  static fn new(x: float, y: float) -> vec2
+
+  fn dot(other: vec2) -> float
+  fn length() -> float
+  fn distance(other: vec2) -> float
+}
+```
+
+### 5.3 Example: `pixel`
+
+`pixel` is also a fixed-layout aggregate builtin type.
+
+- Semantic meaning: position + color
+- Physical layout: 3 slots
+
+Illustrative shape:
+
+```text
+builtin type pixel {
+  layout: [int, int, color]
+
+  field x: int @slot(0)
+  field y: int @slot(1)
+  field color: color @slot(2)
+
+  static fn new(x: int, y: int, color: color) -> pixel
+}
+```
+
+The key point is that `pixel` is still a first-class type in the language even
+though it occupies three stack slots physically.
+
+## 6. Frontend Contract
+
+Frontend languages should expose builtin types through a builtin registry or
+prelude, not through normal user modules.
+
+The frontend may present syntax such as:
+
+- `vec2`
+- `vec2.new(1.0, 2.0)`
+- `v.x`
+- `v.dot(other)`
+
+But user code must not provide the implementation body of builtin members.
+
+The frontend owns:
+
+- syntax
+- name resolution
+- type checking
+- lowering decisions
+
+The frontend does not own:
+
+- builtin semantics
+- builtin numeric algorithms
+- host integration behavior
+
+### 6.1 Builtin declarations are semantic shells
+
+For FE purposes, a builtin declaration behaves like an interface or shell with
+no user body.
+
+For example:
+
+```text
+builtin type vec2 {
+  field x: float
+  field y: float
+
+  static fn new(x: float, y: float) -> vec2
+  fn dot(other: vec2) -> float
+}
+```
+
+The frontend uses this declaration to type-check source programs, but lowering
+must map each member access to VM-defined behavior.
+
+## 7. Lowering Rules
+
+### 7.1 Construction
+
+Construction of a builtin aggregate does not necessarily require a VM
+intrinsic.
+
+If the physical layout is already the canonical stack layout, the frontend may
+lower construction to ordinary pushes or tuple shaping.
+
+Examples:
+
+- `vec2.new(x, y)` -> push `x`, push `y`
+- `pixel.new(x, y, c)` -> push `x`, push `y`, push `c`
+
+The constructor remains semantically builtin even if its lowering is a pure
+layout operation.
+
+### 7.2 Field projection
+
+Field projection also does not necessarily require a VM intrinsic.
+
+If a builtin type has a fixed stack layout, the frontend may lower field access
+through canonical slot projection rules.
+
+Examples:
+
+- `vec2.x` -> project slot 0
+- `vec2.y` -> project slot 1
+- `pixel.color` -> project slot 2
+
+If projection requires non-trivial stack reshaping, the compiler may emit
+helper stack operations or a dedicated intrinsic. The semantic rule remains the
+same.
+
+### 7.3 Domain behavior
+
+Operations whose meaning belongs to the builtin domain should lower to
+intrinsics.
+
+Examples:
+
+- `v1.dot(v2)` -> intrinsic
+- `v.length()` -> intrinsic
+- `v.distance(other)` -> intrinsic
+
+This is the core reason intrinsics exist: the semantics of these operations
+must be owned by the VM rather than by frontend-emitted helper code.
+
+## 8. Intrinsic Identity
+
+Intrinsics should be language-independent.
+
+A canonical identity should use:
+
+```text
+(owner, name, version)
+```
+
+Examples:
+
+- `("color", "rgb", 1)`
+- `("vec2", "dot", 1)`
+- `("vec2", "length", 1)`
+- `("vec2", "distance", 1)`
+
+`owner` may be:
+
+- a builtin type name, such as `vec2`
+- a builtin namespace, if needed later
+
+This identity is used by the frontend and by any optional preload artifact
+format. The VM may execute a compact numeric intrinsic id after resolution.
+
+## 9. Intrinsic Metadata
+
+The VM should own a canonical intrinsic registry.
+
+Illustrative shape:
+
+```text
+IntrinsicMeta {
+  id: u32
+  owner: string
+  name: string
+  version: u16
+  arg_layout: [AbiType]
+  ret_layout: [AbiType]
+  deterministic: bool
+  may_allocate: bool
+  cost_hint: u32
+}
+```
+
+`AbiType` must describe physical slot layout, not just source syntax.
+
+Illustrative shape:
+
+```text
+AbiType =
+  Int32
+  Int64
+  Float64
+  Bool
+  String
+  Handle
+  Color
+  Aggregate([AbiType])
+```
+
+Examples:
+
+- `color` -> `Color`
+- `vec2` -> `Aggregate([Float64, Float64])`
+- `pixel` -> `Aggregate([Int32, Int32, Color])`
+
+Flattening into slots is canonical. For verifier purposes:
+
+- `Color` consumes 1 slot
+- `Aggregate([Float64, Float64])` consumes 2 slots
+- `Aggregate([Int32, Int32, Color])` consumes 3 slots
+
+## 10. Bytecode Model
+
+This specification recommends a distinct intrinsic instruction path.
+
+Illustrative final executable form:
+
+```text
+INTRINSIC <id>
+```
+
+The VM interprets `<id>` using the intrinsic registry.
+
+An optional preload artifact may use a declaration table, similar to syscall
+resolution:
+
+```text
+INTRCALL <decl_index>
+```
+
+with:
+
+```text
+IntrinsicDecl {
+  owner: string
+  name: string
+  version: u16
+}
+```
+
+The loader may then resolve:
+
+```text
+INTRCALL <decl_index> -> INTRINSIC <id>
+```
+
+This mirrors syscall resolution without introducing host coupling.
+
+If the implementation prefers, PBS may also emit final `INTRINSIC <id>`
+directly once the intrinsic registry is stable.
+
+## 11. Verifier Rules
+
+The verifier must treat intrinsics as first-class stack effects with known
+layouts.
+
+For each intrinsic, the verifier must know:
+
+1. input slot count
+2. output slot count
+3. slot layout
+4. whether allocation is allowed
+
+Example:
+
+```text
+vec2.dot(vec2, vec2) -> float
+```
+
+Canonical flattened layout:
+
+- args: `[float, float, float, float]`
+- returns: `[float]`
+
+So verifier stack effect is:
+
+```text
+pop 4, push 1
+```
+
+Another example:
+
+```text
+pixel.new(int, int, color) -> pixel
+```
+
+Flattened layout:
+
+- args: `[int, int, color]`
+- returns: `[int, int, color]`
+
+This may be lowered as:
+
+- no-op stack shaping, or
+- a constructor intrinsic with `pop 3, push 3`
+
+The verifier must reason about the actual lowered form.
+
+## 12. Determinism Rules
+
+Intrinsic behavior must be VM-canonical.
+
+This means:
+
+1. Intrinsics must not call the host.
+2. Intrinsics must not depend on wall-clock time.
+3. Intrinsics must not depend on frontend-generated helper algorithms.
+4. Numeric behavior must be specified tightly enough for portability.
+
+This matters especially for floating-point operations such as:
+
+- `vec2.length`
+- `vec2.distance`
+
+If the platform requires strong cross-host determinism, the VM must define the
+numeric behavior precisely enough to avoid backend drift. Depending on the final
+design, that may mean:
+
+- canonical floating-point rules
+- constrained instruction sequences
+- fixed-point math for some domains
+
+The important requirement is semantic ownership by the VM.
+
+## 13. Separation from HAL
+
+Builtin types must not be defined by HAL types.
+
+Correct layering:
+
+1. PBS and the VM define builtin semantic types.
+2. The VM defines intrinsic behavior.
+3. Syscalls bridge VM values to host services.
+4. The HAL adapts host/runtime values to device-specific behavior.
+
+For example:
+
+- `color` is a VM builtin type
+- `gfx.clear(color)` is a syscall using a `color` argument
+- the host runtime converts that value into any HAL-specific color adapter
+
+The HAL may consume builtin values, but it must not own their language-level
+definition.
+
+## 14. Recommended Initial Scope
+
+A minimal first wave should support:
+
+1. Scalar builtin type:
+   - `color`
+2. Aggregate builtin types:
+   - `vec2`
+   - `pixel`
+3. Intrinsic-only domain methods for `vec2`:
+   - `dot`
+   - `length`
+   - `distance`
+
+Initial constructor and field access lowering may remain compiler-driven when
+they are pure layout operations.
+
+## 15. Summary
+
+This proposal establishes the following model:
+
+1. Builtin types are first-class language types with canonical slot layouts.
+2. Stack-only builtin aggregates are valid even when they occupy multiple slots.
+3. Frontends expose builtin declarations as semantic shells, not as user-
+   implemented code.
+4. Construction and field projection may lower directly to canonical stack
+   layout operations.
+5. Builtin domain behavior lowers to VM intrinsics.
+6. Syscalls remain exclusively for host-backed behavior.
+7. The VM, not the frontend or HAL, owns the semantics of builtin operations.
diff --git a/docs/specs/pbs/10. Memory and Lifetime Specification.md b/docs/specs/pbs/10. Memory and Lifetime Specification.md
new file mode 100644
index 00000000..7e413557
--- /dev/null
+++ b/docs/specs/pbs/10. Memory and Lifetime Specification.md	
@@ -0,0 +1,131 @@
+# PBS Memory and Lifetime Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: runtime memory spaces, value representation classes, identity, aliasing, GC baseline, and host-memory boundaries in PBS core
+
+## 1. Purpose
+
+This document will define the authoritative PBS memory and lifetime model for v1.
+
+Its purpose is to make the language's runtime storage model explicit enough that:
+
+- implementations agree on which values are heap-backed,
+- identity and aliasing are not left implicit,
+- GC remains compatible with deterministic execution,
+- the VM heap and host-owned memory boundary stay understandable,
+- tooling can surface runtime-visible memory and allocation costs consistently.
+
+## 2. Scope
+
+This document is intended to define:
+
+- runtime memory spaces relevant to PBS user semantics,
+- value categories and their representation classes,
+- identity, aliasing, and copy behavior,
+- baseline GC guarantees and non-guarantees,
+- host-memory boundary rules,
+- memory-related safety invariants and remaining runtime failure boundaries,
+- hooks that later diagnostics and tooling may rely on for cost reporting.
+
+This document does not define:
+
+- exact GC algorithm internals,
+- general-purpose allocator APIs,
+- future explicit lifetime syntax activation,
+- final IR lowering details,
+- subsystem-specific host resource APIs.
+
+## 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. `1. Language Charter.md`
+4. `3. Core Syntax Specification.md`
+5. `4. Static Semantics Specification.md`
+6. `9. Dynamic Semantics Specification.md`
+7. 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`
+- `9. Dynamic Semantics Specification.md`
+
+This document is expected to be closed using decisions from:
+
+- `docs/agendas/Heap Model - Agenda.md`
+- `docs/agendas/Memory and Lifetime - Agenda.md`
+- `docs/agendas/Dynamic Semantics - Execution Model Agenda.md`
+- `docs/agendas/Dynamic Semantics - Effect Surfaces Agenda.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- Struct values are heap-backed reference values in v1 core.
+- Assigning a struct value copies the reference, not the underlying field storage.
+- Service values are canonical module-owned singleton values in v1 core.
+- Assigning a service value copies the same singleton identity and does not create a new instance.
+- `declare const` values are compile-time constants rather than mutable runtime module storage.
+- Advanced memory syntax such as `alloc`, `borrow`, `mutate`, `peek`, `take`, and `weak` is not active in PBS core v1.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. runtime memory spaces,
+2. value representation classes,
+3. identity and aliasing,
+4. copy and passing behavior,
+5. GC guarantees and safepoint constraints,
+6. host-memory boundary rules,
+7. memory-related safety properties,
+8. cost visibility hooks consumed by diagnostics/tooling.
+
+## 7. A Ver
+
+The following items remain to be closed in agenda discussion before this document can be considered complete.
+
+### 7.1 `Memory and Lifetime - Agenda.md`
+
+- Heap residency by value category beyond already-settled struct and service behavior.
+- Which values have stable user-visible identity.
+- Exact aliasing story for tuples, callbacks, collections, `optional`, and `result<E>`.
+- Normative GC guarantees versus implementation-defined GC details.
+- Representation and safety model of host-backed resources and handles.
+
+### 7.2 `Heap Model - Agenda.md`
+
+- Cross-cutting visibility of allocation, copy, retention, and host-boundary costs.
+- Which memory facts are normative versus profiler-quality best effort.
+- Migration policy and activation criteria for reserved lifetime keywords in future profiles.
+
+### 7.3 `Dynamic Semantics - Execution Model Agenda.md` and `Dynamic Semantics - Effect Surfaces Agenda.md`
+
+- Which constructs allocate or retain memory during ordinary execution.
+- Which effect-bearing constructs may trap only because their subexpressions trap.
+- Which safepoints are observable versus implementation detail.
+
+## 8. Non-Goals
+
+- Designing full pool, arena, or weak-reference libraries in this pass.
+- Reintroducing mandatory user-authored lifetime syntax in core v1.
+- Defining exact collector implementation strategy.
+- Rewriting already-settled source syntax.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. every core value category has an explicit representation and aliasing story,
+2. GC guarantees and non-guarantees are separated clearly,
+3. the VM heap versus host-memory boundary is normatively described,
+4. memory-related costs are specified well enough for diagnostics/tooling hooks,
+5. the document no longer relies on unresolved `A Ver` items for ordinary v1 behavior.
diff --git a/docs/specs/pbs/11. Diagnostics Specification.md b/docs/specs/pbs/11. Diagnostics Specification.md
new file mode 100644
index 00000000..383f43d2
--- /dev/null
+++ b/docs/specs/pbs/11. Diagnostics Specification.md	
@@ -0,0 +1,133 @@
+# PBS Diagnostics Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: deterministic diagnostics emitted by PBS-facing tooling across parsing, static analysis, manifest/import resolution, lowering boundaries, and related load-facing validation surfaces
+
+## 1. Purpose
+
+This document will define the PBS diagnostics contract.
+
+Its purpose is to make diagnostics stable enough that:
+
+- conforming tools report failures in the same places,
+- users receive deterministic and actionable feedback,
+- conformance can validate not only acceptance/rejection but also diagnostic class and location,
+- frontend, manifest, and load-facing validation remain aligned.
+
+## 2. Scope
+
+This document is intended to define:
+
+- diagnostic categories and phases,
+- minimum metadata carried by diagnostics,
+- stability expectations for source spans, file attribution, and phase attribution,
+- the normative relationship between syntax/static diagnostics and later lowering/load diagnostics,
+- which diagnostics are required versus implementation-defined enrichments,
+- cost-visibility diagnostics or warnings once memory/effect decisions are closed.
+
+This document does not define:
+
+- the full runtime trap catalog,
+- UI presentation or IDE styling,
+- implementation-specific hint ranking,
+- profiling output formats.
+
+## 3. Authority and Precedence
+
+Normative precedence:
+
+1. `1. Language Charter.md`
+2. `3. Core Syntax Specification.md`
+3. `4. Static Semantics Specification.md`
+4. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+5. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+6. `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+7. `9. Dynamic Semantics Specification.md`
+8. `10. Memory and Lifetime Specification.md`
+9. `12. IR and Lowering Specification.md`
+10. This document
+
+If a diagnostic rule here contradicts a normative acceptance/rejection rule in a higher-precedence document, the higher-precedence document wins.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `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`
+- `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+
+This document will also depend on decisions closed in:
+
+- `9. Dynamic Semantics Specification.md`
+- `10. Memory and Lifetime Specification.md`
+- the future backend agenda sequence tracked in `docs/agendas/`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- The syntax specification already enumerates minimum required syntax diagnostics.
+- The static semantics specification already enumerates minimum required static diagnostics.
+- Manifest/import resolution failures are required to be deterministic compile-time errors.
+- Loader failures around malformed or unauthorized host usage are required to be deterministic.
+- Stable source span metadata is required at the token level and must remain useful to later diagnostics.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. diagnostic phases,
+2. required diagnostic metadata,
+3. span and file attribution,
+4. syntax-diagnostic contract,
+5. static-diagnostic contract,
+6. manifest/import-resolution diagnostics,
+7. lowering and host-binding diagnostics,
+8. load-facing and capability diagnostics,
+9. cost-visibility diagnostics and warnings.
+
+## 7. A Ver
+
+The following items remain to be closed before this document can be considered complete.
+
+### 7.1 Depends on `9. Dynamic Semantics Specification.md`
+
+- Which runtime-observable trap categories need source-facing compile-time or conformance hooks.
+- Which constructs require special diagnostics for abrupt completion, propagation, or effect misuse beyond what static semantics already lists.
+
+### 7.2 Depends on `10. Memory and Lifetime Specification.md`
+
+- Which allocations, copies, escapes, and host-boundary crossings must surface as normative diagnostics or warnings.
+- Which cost facts are mandatory versus implementation-defined enrichment.
+
+### 7.3 Depends on the future backend agenda sequence tracked in `docs/agendas/`
+
+- Whether diagnostic stability includes IR/lowering phase names, artifact offsets, or source maps.
+- How host-binding lowering failures are surfaced back to source locations.
+- Whether verifier/load diagnostics are part of the PBS diagnostics contract directly or only through artifact-facing tooling.
+
+### 7.4 Still to decide inside this document
+
+- Whether diagnostic codes are mandatory in v1.
+- Which portions of human-readable wording are normative versus illustrative.
+- Whether notes/help text are required, optional, or outside conformance.
+- Exact cross-file diagnostic expectations for module/barrel/import failures.
+
+## 8. Non-Goals
+
+- Mandating one UI or IDE presentation style.
+- Freezing a localization strategy in this pass.
+- Turning every optimization hint into a normative diagnostic.
+- Replacing the acceptance/rejection rules already defined elsewhere.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. every required rejection in the current spec set is mapped to a diagnostic phase,
+2. diagnostic metadata and attribution rules are explicit enough for conformance,
+3. cost-visibility expectations are aligned with memory/effect specs,
+4. the document no longer relies on unresolved backend and runtime-facing `A Ver` items for v1 tooling behavior.
diff --git a/docs/specs/pbs/12. IR and Lowering Specification.md b/docs/specs/pbs/12. IR and Lowering Specification.md
new file mode 100644
index 00000000..1e72b41f
--- /dev/null
+++ b/docs/specs/pbs/12. IR and Lowering Specification.md	
@@ -0,0 +1,136 @@
+# PBS IR and Lowering Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: lowering of bound PBS programs into internal compiler IR and runtime-facing artifacts
+
+## 1. Purpose
+
+This document will define the normative lowering contract from PBS source semantics to implementation artifacts.
+
+Its purpose is to make backend-facing behavior explicit enough that:
+
+- different compilers lower the same bound program compatibly,
+- host-binding emission does not drift from frontend resolution,
+- builtin and intrinsic lowering does not drift from VM-owned metadata,
+- later verifier and loader behavior can rely on stable artifact expectations,
+- conformance can test more than parser and binder behavior.
+
+## 2. Scope
+
+This document is intended to define:
+
+- the minimum semantic obligations of the compiler after parsing, binding, and type checking,
+- the role of internal IR as an implementation stage,
+- what semantic facts lowering must preserve,
+- lowering of control flow, calls, callbacks, services, contracts, constants, and host-backed calls,
+- lowering of builtin projections, builtin constants, and intrinsic member calls,
+- artifact-facing requirements that must hold before loader/verifier consumption.
+
+This document does not define:
+
+- the full PBX binary layout,
+- optimizer heuristics or performance tuning strategy,
+- the exact in-memory data structures of one compiler implementation,
+- runtime GC algorithm internals.
+
+## 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. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+6. `6. VM-owned vs Host-backed.md`
+7. `6.1. Intrinsics and Builtin Types Specification.md`
+8. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+9. `9. Dynamic Semantics Specification.md`
+10. `10. Memory and Lifetime Specification.md`
+11. This document
+
+If a lowering rule here contradicts a higher-precedence semantic rule, the higher-precedence rule wins.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `3. Core Syntax Specification.md`
+- `4. Static Semantics Specification.md`
+- `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+- `6. VM-owned vs Host-backed.md`
+- `6.1. Intrinsics and Builtin Types Specification.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `9. Dynamic Semantics Specification.md`
+- `10. Memory and Lifetime Specification.md`
+
+This document is expected to be closed using a future backend agenda sequence tracked in `docs/agendas/`.
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- The compiler consumes reserved `Host` metadata while resolving host-backed SDK members.
+- The compiler consumes reserved `BuiltinType`, `BuiltinConst`, `IntrinsicCall`, and `Slot` metadata while resolving builtin shells.
+- The compiler emits canonical host-binding declarations into the PBX `SYSC` table.
+- The compiler emits host-backed callsites in pre-load form as `HOSTCALL <sysc_index>`.
+- `SYSC` entries are deduplicated by canonical identity and ordered by first occurrence.
+- The loader, not the compiler, resolves canonical host bindings to final numeric syscall identifiers.
+- Builtin projection lowering remains VM-owned and does not emit host-binding metadata.
+- Builtin constants lower through VM-owned materialization rather than through ordinary compile-time constant evaluation.
+- Builtin intrinsic member calls lower through a VM-owned intrinsic path rather than through `SYSC`, `HOSTCALL`, or `SYSCALL`.
+- Stdlib interface modules are compile-time-only and do not emit executable bytecode by themselves.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. lowering preconditions,
+2. semantic obligations preserved by IR,
+3. lowering of expressions and control flow,
+4. lowering of callable categories,
+5. lowering of `optional` and `result<E>` constructs,
+6. lowering of callbacks, services, and contracts,
+7. lowering of builtin projections, builtin constants, and builtin intrinsic calls,
+8. host-binding emission,
+9. artifact invariants required before verifier/loader stages.
+
+## 7. A Ver
+
+The following items remain to be closed before this document can be considered complete.
+
+### 7.1 Depends on `9. Dynamic Semantics Specification.md`
+
+- Which evaluation-order guarantees must be preserved explicitly in lowering.
+- Which traps, abrupt completions, and propagation paths require dedicated lowered forms.
+- Whether callback formation and contract dispatch need dedicated runtime artifacts or only implementation-defined IR shapes.
+
+### 7.2 Depends on `10. Memory and Lifetime Specification.md`
+
+- Which lowered operations allocate, alias, retain, or cross the host-memory boundary.
+- Which runtime storage/identity facts IR must preserve explicitly versus infer later.
+
+### 7.3 Depends on the future backend agenda sequence tracked in `docs/agendas/`
+
+- Whether one canonical IR is normative or only the preserved semantic obligations are normative.
+- The exact mapping from bound PBS constructs to PBX/bytecode-facing artifacts beyond already-settled host-binding and intrinsic behavior.
+- Lowering strategy for services, contracts, callbacks, tuples, and result propagation.
+- Whether declaration-based intrinsic preload forms such as `INTRCALL` are part of v1 lowering or whether compilers should emit final `INTRINSIC <id>` directly for a selected VM line.
+- Which artifact invariants belong here versus a future dedicated PBX/bytecode mapping document.
+
+## 8. Non-Goals
+
+- Freezing one optimizer design.
+- Requiring one compiler implementation architecture.
+- Repeating the full bytecode ISA specification.
+- Defining loader-side patching internals already owned elsewhere.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. every semantically distinct core construct has an explicit lowering story,
+2. the boundary between source semantics, compiler IR, and emitted artifacts is clear,
+3. host-binding emission is fully aligned with the Host ABI spec,
+4. builtin and intrinsic lowering is fully aligned with the VM-owned builtin spec,
+5. the document no longer relies on unresolved backend `A Ver` items for ordinary v1 lowering behavior.
diff --git a/docs/specs/pbs/13. Conformance Test Specification.md b/docs/specs/pbs/13. Conformance Test Specification.md
new file mode 100644
index 00000000..edde23aa
--- /dev/null
+++ b/docs/specs/pbs/13. Conformance Test Specification.md	
@@ -0,0 +1,138 @@
+# PBS Conformance Test Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: conformance obligations, test categories, and acceptance criteria for PBS implementations
+
+## 1. Purpose
+
+This document will define the PBS conformance testing contract.
+
+Its purpose is to make the specification operational by defining:
+
+- what an implementation must demonstrate to claim conformance,
+- which parts of the spec require positive versus negative tests,
+- how deterministic diagnostics and runtime behavior are validated,
+- how compatibility and version claims are checked.
+
+## 2. Scope
+
+This document is intended to define:
+
+- conformance levels or profiles, if any,
+- required test categories,
+- expectations for syntax, static, manifest, lowering, loader, and runtime tests,
+- diagnostic-conformance expectations,
+- artifact and runtime fixtures needed for host-binding and capability-gating tests,
+- compatibility-matrix conformance hooks.
+
+This document does not define:
+
+- one specific test runner implementation,
+- CI policy for one repository,
+- benchmark or performance certification,
+- product release governance process.
+
+## 3. Authority and Precedence
+
+Normative precedence:
+
+1. `1. Language Charter.md`
+2. `2. Governance and Versioning.md`
+3. `3. Core Syntax Specification.md`
+4. `4. Static Semantics Specification.md`
+5. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+6. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+7. `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+8. `9. Dynamic Semantics Specification.md`
+9. `10. Memory and Lifetime Specification.md`
+10. `11. Diagnostics Specification.md`
+11. `12. IR and Lowering Specification.md`
+12. This document
+
+This document must not weaken a normative requirement imposed by higher-precedence specs.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum, the full active PBS v1 spec set.
+
+In the current phase, it should be drafted against:
+
+- `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`
+- `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+
+It will require closure of:
+
+- `9. Dynamic Semantics Specification.md`
+- `10. Memory and Lifetime Specification.md`
+- `11. Diagnostics Specification.md`
+- `12. IR and Lowering Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- The parser must behave deterministically.
+- Syntax and static semantics already enumerate minimum required rejection cases.
+- Import/manifest failures are required to be deterministic.
+- Loader failures for malformed or unauthorized host usage are required to be deterministic.
+- Governance requires conformance updates before release.
+- Compatibility claims must be reflected in a published compatibility matrix.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. scope of conformance,
+2. implementation claims and version domains,
+3. required positive parsing/binding/type-checking tests,
+4. required negative syntax/static tests,
+5. manifest/import-resolution tests,
+6. dynamic-semantics runtime tests,
+7. host-binding and capability-gating tests,
+8. diagnostics-conformance tests,
+9. compatibility and regression test expectations.
+
+## 7. A Ver
+
+The following items remain to be closed before this document can be considered complete.
+
+### 7.1 Depends on `9. Dynamic Semantics Specification.md` and `10. Memory and Lifetime Specification.md`
+
+- Exact runtime-oracle model for observable evaluation order, traps, and effect behavior.
+- Which memory/aliasing facts must be tested directly versus only through diagnostics/tooling hooks.
+
+### 7.2 Depends on `11. Diagnostics Specification.md`
+
+- Whether conformance checks diagnostic codes, spans, categories, wording classes, or only rejection phase and location.
+- Which warnings or cost diagnostics are in conformance scope.
+
+### 7.3 Depends on `12. IR and Lowering Specification.md`
+
+- Whether artifact-level conformance is required in addition to source-level conformance.
+- Which emitted host-binding and lowering invariants require golden tests.
+
+### 7.4 Still to decide inside this document
+
+- Whether PBS v1 has one conformance level or staged claims such as frontend-only versus full toolchain.
+- Fixture strategy for stdlib environments, host registries, and capability-grant scenarios.
+- How compatibility-matrix claims are validated across language/profile/stdlib domains.
+
+## 8. Non-Goals
+
+- Replacing the normative specs with tests as the primary authority.
+- Forcing one repository layout or one test harness.
+- Treating performance benchmarking as language conformance.
+- Inventing new language rules through test-only precedent.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. every active PBS v1 spec has a corresponding conformance surface,
+2. positive and negative obligations are clearly separated,
+3. diagnostics and runtime behavior have explicit oracle expectations,
+4. compatibility and version claims can be tested rather than asserted informally,
+5. the document no longer relies on unresolved `A Ver` items for the intended conformance level.
diff --git a/docs/specs/pbs/14. Name Resolution and Module Linking Specification.md b/docs/specs/pbs/14. Name Resolution and Module Linking Specification.md
new file mode 100644
index 00000000..dd795300
--- /dev/null
+++ b/docs/specs/pbs/14. Name Resolution and Module Linking Specification.md	
@@ -0,0 +1,169 @@
+# PBS Name Resolution and Module Linking Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: scope formation, name lookup, imports, exports, barrel visibility, cross-module resolution, and semantic linking of PBS programs
+
+## 1. Purpose
+
+This document will define the normative name-resolution and semantic-linking model for PBS.
+
+## 2. Scope
+
+This document is intended to define:
+
+- scope formation and lookup order,
+- namespace separation and collision rules,
+- import and export resolution,
+- barrel-mediated visibility and module linking,
+- cross-file and cross-module symbol resolution,
+- resolution of reserved stdlib shells for host-backed and VM-owned surfaces,
+- linkage-time rejection conditions before lowering.
+
+This document does not define:
+
+- runtime execution behavior,
+- optimizer or backend internals,
+- full PBX binary linking.
+
+## 3. Authority and Precedence
+
+Normative precedence:
+
+1. `3. Core Syntax Specification.md`
+2. `4. Static Semantics Specification.md`
+3. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+4. `6. VM-owned vs Host-backed.md`
+5. `6.1. Intrinsics and Builtin Types Specification.md`
+6. `18. Standard Library Surface Specification.md`
+7. This document
+
+If a rule here conflicts with higher-precedence specs, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `3. Core Syntax Specification.md`
+- `4. Static Semantics Specification.md`
+- `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+- `6. VM-owned vs Host-backed.md`
+- `6.1. Intrinsics and Builtin Types Specification.md`
+- `8. Stdlib Environment Packaging and Loading Specification.md`
+- `18. Standard Library Surface Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- PBS has distinct type, value, callable, and host-owner namespaces.
+- `mod.barrel` is the single source of module visibility.
+- Imports target modules, not files.
+- Reserved stdlib project spaces are resolved only from the selected stdlib environment.
+- Only `pub` symbols may be imported from another module.
+- Reserved stdlib/interface modules may expose compile-time-only shells for both host-backed and VM-owned surfaces.
+- Source-visible builtin names are resolved through imported builtin shell declarations rather than by hardcoded source spelling alone.
+- Canonical builtin identity and canonical intrinsic identity are governed by builtin metadata rather than by the imported PBS-visible declaration name alone.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. scope construction,
+2. lookup order by namespace,
+3. import and alias resolution,
+4. barrel export matching and linking,
+5. reserved stdlib shell resolution for builtin and host-backed surfaces,
+6. duplicate and shadowing rules,
+7. cross-module resolution failures.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Exact lookup order across local bindings, top-level declarations, imports, and reserved intrinsic surfaces.
+- Whether shadowing rules differ by namespace or declaration kind.
+- Whether semantic linking is fully part of static semantics or split into a distinct phase contract.
+- Exact rejection model for ambiguous cross-module overload visibility and barrel-linked callable sets.
+- Whether stdlib/interface-module linking imposes extra restrictions beyond ordinary modules.
+- Whether builtin shell declarations may be synthesized by the toolchain in addition to being provided by stdlib modules.
+
+## 8. Non-Goals
+
+- Reopening the already-settled import surface syntax.
+- Defining runtime loader behavior.
+- Freezing one compiler symbol-table implementation.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. name lookup is deterministic across all relevant scopes,
+2. barrel and module linking behavior is explicit,
+3. reserved stdlib shell resolution is explicit for host-backed and VM-owned surfaces,
+4. cross-module ambiguity and failure cases are normatively defined,
+5. the document no longer relies on unresolved `A Ver` items for ordinary v1 resolution behavior.
+
+## 10. Reserved Stdlib Shell Resolution
+
+Reserved stdlib modules may expose compile-time-only declarations that do not
+behave like ordinary user-authored implementation bodies.
+
+Rules:
+
+- `declare host` surfaces exported from reserved stdlib modules resolve in the host-owner namespace.
+- `declare builtin type` surfaces exported from reserved stdlib modules resolve in the type namespace.
+- builtin constants exported from reserved stdlib modules resolve in the value namespace.
+- builtin intrinsic methods are not imported as free functions; they are resolved through the imported builtin type declaration of the receiver type.
+- canonical host identity is not derived from the imported host owner spelling,
+- and canonical builtin/intrinsic identity is not derived solely from the imported builtin type spelling.
+
+Example:
+
+- importing `Vec2` from `@core:math` may introduce the PBS-visible type name `Vec2`,
+- while the declaration's metadata may still lower that type to canonical builtin identity `("vec2", 1)`.
+
+## 11. Import and Barrel Rules for Builtin Shells
+
+Builtin shells follow ordinary module visibility rules at the source level and
+special metadata rules at lowering time.
+
+Rules:
+
+- a builtin type, builtin constant, or host owner may be imported only if it is exported through the target module's `mod.barrel`,
+- aliasing an imported builtin type changes only the source-visible local name, not the canonical builtin identity declared by metadata,
+- aliasing an imported builtin constant changes only the local binding name, not the canonical builtin constant identity declared by metadata,
+- aliasing an imported host owner changes only the source-visible local name, not the canonical host identity declared by `Host(...)`,
+- barrel matching for builtin declarations is declaration-based rather than executable-body based,
+- and resolution must complete before lowering begins.
+
+## 12. Lookup Order for Builtin and Intrinsic Surfaces
+
+Lookup remains namespace-based.
+
+Rules:
+
+- type-position lookup considers visible builtin type declarations alongside other visible type declarations,
+- value-position lookup considers visible builtin constants alongside other visible values,
+- callable lookup does not treat builtin intrinsic members as top-level callable declarations,
+- member lookup on a builtin-typed receiver considers builtin projection fields first as field-like surfaces of that builtin declaration,
+- method lookup on a builtin-typed receiver considers builtin intrinsic member signatures declared by that builtin shell,
+- and host-owner lookup remains separate from builtin type lookup.
+
+This preserves the distinction between:
+
+- imported builtin type shells,
+- imported host owners,
+- and compiler-recognized intrinsic method surfaces on existing core forms such as `optional` and enums.
+
+## 13. Deterministic Resolution Failures
+
+At minimum, a conforming implementation must reject:
+
+1. import of a non-exported builtin type shell,
+2. import of a non-exported builtin constant shell,
+3. import of a non-exported host owner shell,
+4. ambiguous cross-module visibility of builtin declarations after barrel resolution,
+5. duplicate visible builtin type declarations that claim the same canonical builtin identity in one resolved environment,
+6. duplicate visible builtin constants that claim the same canonical builtin constant identity in one resolved environment,
+7. member lookup on a builtin receiver where the imported builtin shell does not declare the requested field or intrinsic member,
+8. any resolution path that attempts to derive host or builtin canonical identity from alias spelling alone.
diff --git a/docs/specs/pbs/15. Bytecode and PBX Mapping Specification.md b/docs/specs/pbs/15. Bytecode and PBX Mapping Specification.md
new file mode 100644
index 00000000..795dcf21
--- /dev/null
+++ b/docs/specs/pbs/15. Bytecode and PBX Mapping Specification.md	
@@ -0,0 +1,92 @@
+# PBS Bytecode and PBX Mapping Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: mapping from lowered PBS programs into PBX sections, bytecode-facing artifacts, and related source-to-artifact invariants
+
+## 1. Purpose
+
+This document will define the normative mapping between lowered PBS semantics and emitted PBX/bytecode-facing artifacts.
+
+## 2. Scope
+
+This document is intended to define:
+
+- artifact-level obligations after lowering,
+- mapping of semantic constructs into PBX-visible structures,
+- source-to-artifact invariants required by verifier and loader stages,
+- interaction points with host-binding metadata such as `SYSC`,
+- interaction points with VM-owned builtin and intrinsic metadata.
+
+This document does not define:
+
+- the full bytecode ISA,
+- UI/tooling presentation,
+- one compiler's internal IR representation.
+
+## 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. `6.1. Intrinsics and Builtin Types Specification.md`
+4. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+5. `12. IR and Lowering Specification.md`
+6. This document
+
+If a rule here conflicts with higher-precedence authorities, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `6.1. Intrinsics and Builtin Types Specification.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `12. IR and Lowering Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- The compiler emits host-binding declarations into PBX `SYSC`.
+- Host-backed callsites are emitted in pre-load form as `HOSTCALL <sysc_index>`.
+- `SYSC` entries are deduplicated by canonical identity and ordered by first occurrence.
+- The loader resolves host bindings and rewrites `HOSTCALL` into `SYSCALL`.
+- VM-owned builtin projections, builtin constants, and intrinsic callsites do not emit host-binding metadata.
+- VM-owned intrinsic artifacts are distinct from `SYSC`, `HOSTCALL`, and `SYSCALL`.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. artifact mapping goals,
+2. section-level invariants,
+3. callsite and control-flow mapping invariants,
+4. metadata mapping obligations,
+5. intrinsic and builtin artifact obligations,
+6. source-attribution hooks for diagnostics/conformance.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Which PBX sections beyond `SYSC` are part of the PBS-facing contract.
+- Whether a distinct intrinsic declaration section is part of the PBS-facing contract in v1.
+- Which source-level constructs require dedicated artifact patterns versus implementation freedom.
+- How much of artifact ordering, numbering, and layout is normative at PBS level versus owned purely by PBX authority.
+- Whether compilers should emit final `INTRINSIC <id>` directly for a selected VM line or may emit a declaration-based preload form such as `INTRCALL <decl_index>`.
+- Whether a separate debug/source-map surface is part of v1.
+
+## 8. Non-Goals
+
+- Repeating the full PBX or ISA documentation.
+- Mandating one binary-emitter implementation strategy.
+- Defining loader patching internals already owned elsewhere.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. the PBS-to-artifact boundary is explicit,
+2. artifact-level invariants needed by verifier and loader are normative,
+3. the document no longer relies on unresolved `A Ver` items for ordinary v1 artifact mapping behavior.
diff --git a/docs/specs/pbs/16. Runtime Execution and Initialization Specification.md b/docs/specs/pbs/16. Runtime Execution and Initialization Specification.md
new file mode 100644
index 00000000..3f8153c7
--- /dev/null
+++ b/docs/specs/pbs/16. Runtime Execution and Initialization Specification.md	
@@ -0,0 +1,91 @@
+# PBS Runtime Execution and Initialization Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: runtime startup, entry behavior, module/service initialization, and execution lifecycle of PBS programs after successful load
+
+## 1. Purpose
+
+This document will define the runtime execution and initialization contract for PBS programs.
+
+## 2. Scope
+
+This document is intended to define:
+
+- entry and startup behavior,
+- initialization ordering relevant to PBS-visible semantics,
+- lifecycle of module-owned and service-owned runtime state,
+- execution boundaries before, during, and after frame-driven program operation,
+- runtime assumptions that are neither purely dynamic semantics nor purely loader behavior.
+
+This document does not define:
+
+- loader-side host resolution,
+- full packaging format,
+- scheduler models outside v1 execution assumptions.
+
+## 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. `1. Language Charter.md`
+3. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+4. `9. Dynamic Semantics Specification.md`
+5. `10. Memory and Lifetime Specification.md`
+6. This document
+
+If a rule here conflicts with higher-precedence authorities, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `1. Language Charter.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+- `9. Dynamic Semantics Specification.md`
+- `10. Memory and Lifetime Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- `FRAME_SYNC`-based execution semantics are preserved.
+- Loader-side host binding resolution and capability gating happen before program execution begins.
+- Service values are canonical module-owned singleton values.
+- Top-level executable statements are forbidden in PBS source modules.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. execution entry assumptions,
+2. initialization ordering,
+3. service singleton runtime lifecycle,
+4. runtime frame and step boundaries,
+5. failure and non-start conditions.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Exact runtime entry contract between loaded artifact and PBS-visible program behavior.
+- Whether module initialization exists as a distinct semantic phase in v1 beyond load success.
+- When service singleton state becomes initialized and observable.
+- Which runtime lifecycle boundaries are observable to user code versus VM-internal.
+- Whether shutdown/finalization behavior has any PBS-visible contract in v1.
+
+## 8. Non-Goals
+
+- Defining OS/process lifecycle outside Prometeu runtime authority.
+- Reopening the ban on top-level executable statements.
+- Designing a future async runtime.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. runtime startup and initialization order are normatively described,
+2. service and module runtime lifecycle assumptions are explicit,
+3. execution lifecycle boundaries are aligned with dynamic semantics and runtime authority,
+4. the document no longer relies on unresolved `A Ver` items for ordinary v1 runtime startup behavior.
diff --git a/docs/specs/pbs/17. Compatibility and Evolution Policy.md b/docs/specs/pbs/17. Compatibility and Evolution Policy.md
new file mode 100644
index 00000000..90628b56
--- /dev/null
+++ b/docs/specs/pbs/17. Compatibility and Evolution Policy.md	
@@ -0,0 +1,90 @@
+# PBS Compatibility and Evolution Policy
+
+Status: Draft v0 (Skeleton)  
+Applies to: compatibility commitments, migration boundaries, deprecation discipline, and evolution constraints across PBS language and related domains
+
+## 1. Purpose
+
+This document will define the normative compatibility and evolution policy for PBS.
+
+## 2. Scope
+
+This document is intended to define:
+
+- compatibility promises across language, profile, stdlib, and artifact domains,
+- migration boundaries for additive versus incompatible changes,
+- deprecation and removal policy details,
+- behavioral versus binary compatibility expectations,
+- obligations when publishing changes that affect older cartridges or projects.
+
+This document does not define:
+
+- one repository's release workflow,
+- one implementation's branching strategy,
+- detailed changelog formatting.
+
+## 3. Authority and Precedence
+
+Normative precedence:
+
+1. `1. Language Charter.md`
+2. `2. Governance and Versioning.md`
+3. Runtime and bytecode authority where applicable
+4. This document
+
+If a rule here conflicts with higher-precedence authorities, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `1. Language Charter.md`
+- `2. Governance and Versioning.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `7. Cartridge Manifest and Runtime Capabilities Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- Additive-first evolution is preferred for minor releases.
+- Incompatible changes belong only in major lines with migration guidance.
+- Canonical host primitive versioning uses `(module, name, version)`.
+- Toolchains must reject unsupported targets deterministically.
+- Older supported cartridges are expected to keep running across updates.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. compatibility domains,
+2. behavioral versus binary compatibility,
+3. deprecation windows,
+4. migration obligations,
+5. compatibility-matrix expectations,
+6. artifact and runtime compatibility boundaries.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Exact compatibility window by domain.
+- Whether PBX/binary compatibility has an independent policy track from source-level compatibility.
+- How stdlib-line compatibility interacts with dependency projects over time.
+- Which changes require migration tooling versus documentation-only migration notes.
+- Whether frontend-only phased implementation claims need distinct compatibility labels.
+
+## 8. Non-Goals
+
+- Replacing governance with ad hoc decisions.
+- Defining one product release calendar.
+- Freezing every editorial clarification as a compatibility event.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. compatibility commitments are explicit by domain,
+2. deprecation and migration duties are normatively described,
+3. source, stdlib, artifact, and runtime compatibility boundaries are separated clearly,
+4. the document no longer relies on unresolved `A Ver` items for ordinary v1 compatibility claims.
diff --git a/docs/specs/pbs/18. Standard Library Surface Specification.md b/docs/specs/pbs/18. Standard Library Surface Specification.md
new file mode 100644
index 00000000..4a916e9b
--- /dev/null
+++ b/docs/specs/pbs/18. Standard Library Surface Specification.md	
@@ -0,0 +1,185 @@
+# PBS Standard Library Surface Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: normative stdlib-facing API surface, reserved stdlib project spaces, and versioned standard-library contracts exposed to PBS programs
+
+## 1. Purpose
+
+This document will define the normative user-facing standard-library surface for PBS.
+
+## 2. Scope
+
+This document is intended to define:
+
+- what counts as part of the PBS stdlib contract,
+- how stdlib modules are grouped and versioned,
+- which APIs are normative versus implementation-private,
+- how VM-owned builtin shells are exposed to user code,
+- how reserved stdlib project spaces expose user-facing surfaces over host-backed capabilities.
+
+This document does not define:
+
+- one physical packaging layout,
+- registry/publication mechanics,
+- host loader behavior,
+- implementation-private helper modules.
+
+## 3. Authority and Precedence
+
+Normative precedence:
+
+1. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+2. `8. Stdlib Environment Packaging and Loading Specification.md`
+3. `6. VM-owned vs Host-backed.md`
+4. `6.1. Intrinsics and Builtin Types Specification.md`
+5. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+6. This document
+
+If a rule here conflicts with higher-precedence specs, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+- `6. VM-owned vs Host-backed.md`
+- `6.1. Intrinsics and Builtin Types Specification.md`
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `8. Stdlib Environment Packaging and Loading Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- Reserved stdlib project spaces include `@sdk:*` and `@core:*`.
+- Stdlib interface modules are compile-time-only and loaded as PBS-like modules.
+- User code must import stdlib modules explicitly.
+- Canonical host identity comes from reserved host-binding metadata, not from source owner spelling.
+- VM-owned builtin type, builtin constant, and intrinsic surfaces may be exposed through reserved stdlib shells without transferring semantic ownership away from the VM.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. stdlib contract boundaries,
+2. reserved stdlib project spaces and module families,
+3. normative versus non-normative API surfaces,
+4. VM-owned builtin shells exposed to user code,
+5. host-backed SDK surfaces exposed to user code,
+6. versioning and deprecation expectations for stdlib APIs.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Which stdlib modules are mandatory in each active stdlib line.
+- Which APIs are part of the normative core teaching surface versus optional library growth.
+- Whether `@core:*` is specified as language-adjacent utility surface or as ordinary stdlib contract.
+- How stdlib API evolution is documented and conformance-tested.
+- Whether some interface modules remain toolchain-private and outside user-facing stdlib surface.
+- Whether builtin shells may appear in `@sdk:*` as well as `@core:*`, or whether `@sdk:*` should remain host-facing only by policy.
+
+## 8. Non-Goals
+
+- Replacing the resolution/packaging specs.
+- Defining all future libraries in one pass.
+- Hardcoding one distribution format.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. the normative user-facing stdlib surface is explicitly bounded,
+2. reserved project-space API responsibilities are clear,
+3. VM-owned and host-backed stdlib surfaces are explicitly separated,
+4. stdlib versioning and deprecation expectations are aligned with compatibility policy,
+5. the document no longer relies on unresolved `A Ver` items for ordinary v1 stdlib contract claims.
+
+## 10. Reserved Project-Space Responsibilities
+
+The current stdlib direction distinguishes two user-facing reserved spaces.
+
+### 10.1 `@core:*`
+
+`@core:*` is the preferred surface for VM-owned declarations that belong to the
+language-adjacent semantic platform.
+
+Examples:
+
+- builtin type shells,
+- builtin constants,
+- and other VM-owned helper declarations that are not host capability surfaces.
+
+### 10.2 `@sdk:*`
+
+`@sdk:*` is the preferred surface for host-backed capability-facing APIs.
+
+Examples:
+
+- `declare host` surfaces,
+- capability-facing wrappers over host services,
+- and domain SDK modules whose execution meaning ultimately depends on host-backed operations.
+
+Rules:
+
+- source packaging location is part of the stdlib contract surface,
+- but ownership remains governed by the VM-owned vs host-backed classification,
+- and placing a builtin shell in stdlib does not make it host-backed.
+
+## 11. Builtin Shell Surfaces
+
+Reserved stdlib modules may expose builtin declarations as compile-time-only
+shells.
+
+Rules:
+
+- stdlib builtin shells may expose `declare builtin type` declarations,
+- stdlib builtin shells may expose reserved `declare const` declarations carrying `BuiltinConst(...)`,
+- stdlib builtin shells may expose builtin methods carrying `IntrinsicCall(...)`,
+- these shells exist for import, name resolution, type checking, and lowering,
+- and these shells do not provide executable PBS bodies for builtin behavior.
+
+Stdlib is therefore the delivery surface, not the semantic owner.
+
+## 12. Host-backed SDK Surfaces
+
+Reserved stdlib modules may expose host-backed declarations as compile-time-only
+shells.
+
+Rules:
+
+- host-backed stdlib surfaces use `declare host`,
+- host-backed method signatures carry `Host(...)`,
+- user code may import those host owners through ordinary stdlib module imports,
+- and lowering continues through canonical host identity, `SYSC`, `HOSTCALL`, loader resolution, and final `SYSCALL`.
+
+## 13. Stdlib Contract Expectations for Builtin MVP
+
+For the current builtin MVP, stdlib should be able to expose at least:
+
+1. a builtin type shell for `Color`,
+2. a builtin type shell for `Vec2`,
+3. a builtin type shell for `Pixel`,
+4. a builtin constant shell for `vec2.zero`,
+5. and any associated documentation-level or teaching-level module organization needed to make those surfaces discoverable.
+
+Illustrative example:
+
+```pbs
+import { Vec2, ZERO } from @core:math;
+```
+
+The imported names are source-visible conveniences.
+Their canonical runtime-facing identities still come from builtin metadata such
+as `BuiltinType(name="vec2", version=1)` and
+`BuiltinConst(target="vec2", name="zero", version=1)`.
+
+## 14. Deterministic Stdlib Surface Failures
+
+At minimum, a conforming implementation must reject:
+
+1. a stdlib builtin shell that attempts to use host-binding metadata for VM-owned intrinsic behavior,
+2. a stdlib host shell that attempts to use builtin metadata in place of host-binding metadata,
+3. a user-facing stdlib module that exports executable PBS bodies for builtin semantics,
+4. a stdlib line that exposes conflicting canonical builtin identities through the same resolved environment,
+5. a stdlib line that exposes conflicting canonical host identities through the same resolved environment.
diff --git a/docs/specs/pbs/19. Verification and Safety Checks Specification.md b/docs/specs/pbs/19. Verification and Safety Checks Specification.md
new file mode 100644
index 00000000..f7d137d1
--- /dev/null
+++ b/docs/specs/pbs/19. Verification and Safety Checks Specification.md	
@@ -0,0 +1,88 @@
+# PBS Verification and Safety Checks Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: verifier-facing safety obligations, artifact validation boundaries, and the division of safety checks across compiler, loader, verifier, and runtime
+
+## 1. Purpose
+
+This document will define the verification and safety-check model relevant to PBS-produced artifacts.
+
+## 2. Scope
+
+This document is intended to define:
+
+- which safety obligations are enforced before runtime execution,
+- the division of responsibility across compiler, loader, verifier, and runtime,
+- verifier-facing assumptions about already-lowered artifacts,
+- safety properties that must hold for conforming PBS-produced images.
+
+This document does not define:
+
+- full runtime trap semantics,
+- source-language typing rules already owned elsewhere,
+- one verifier implementation architecture.
+
+## 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. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+4. `12. IR and Lowering Specification.md`
+5. `15. Bytecode and PBX Mapping Specification.md`
+6. This document
+
+If a rule here conflicts with higher-precedence authorities, it is invalid.
+
+## 4. Normative Inputs
+
+This document depends on, at minimum:
+
+- `6.2. Host ABI Binding and Loader Resolution Specification.md`
+- `12. IR and Lowering Specification.md`
+- `15. Bytecode and PBX Mapping Specification.md`
+
+## 5. Already-Settled Inputs
+
+The following inputs are already fixed elsewhere and must not be contradicted here:
+
+- Loader-side ABI validation is mandatory.
+- Capability gating is mandatory during load.
+- The verifier runs after loader patching on the final numeric executable image.
+- Loader and verifier validate different layers of the contract.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. safety-check phase boundaries,
+2. compiler-emitted safety assumptions,
+3. loader-side safety checks,
+4. verifier-side safety checks,
+5. residual runtime safety assumptions,
+6. required deterministic rejection conditions.
+
+## 7. A Ver
+
+The following items remain to be closed in future agenda discussion.
+
+- Exact verifier obligations beyond what is already implied by runtime/bytecode authority.
+- Which safety properties must be proven before execution versus checked defensively at runtime.
+- Whether PBS-level conformance includes explicit verifier test surfaces or only artifact validity outcomes.
+- How source-level diagnostics relate to verifier and artifact-level safety failures.
+
+## 8. Non-Goals
+
+- Replacing runtime or bytecode authority.
+- Duplicating the full Host ABI spec.
+- Freezing one verifier implementation algorithm.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. the division of safety responsibilities is explicit,
+2. verifier-facing assumptions are aligned with lowering and artifact mapping,
+3. deterministic rejection surfaces are normatively described,
+4. the document no longer relies on unresolved `A Ver` items for ordinary v1 safety claims.
diff --git a/docs/specs/pbs/3. Core Syntax Specification.md b/docs/specs/pbs/3. Core Syntax Specification.md
index f27a105e..1a351093 100644
--- a/docs/specs/pbs/3. Core Syntax Specification.md	
+++ b/docs/specs/pbs/3. Core Syntax Specification.md	
@@ -248,6 +248,7 @@ Rules:
 - In v1 core, ordinary user-authored modules MUST reject attributes unless another specification explicitly permits them.
 - Reserved stdlib/toolchain interface modules MAY use attributes where explicitly allowed by syntax and semantics.
 - Attribute interpretation is compile-time only unless another specification explicitly lowers its effect into runtime-facing metadata.
+- Reserved attribute names used by builtin-type and intrinsic shells do not become ordinary value-level syntax.
 
 ### 6.2 Top-level declarations
 
@@ -256,29 +257,34 @@ TopDecl ::= TypeDecl | CallbackDecl | FunctionDecl | ConstDecl | ImplDecl
 ```
 
 Top-level `let` forms and top-level executable statements are forbidden.
-`declare host` is reserved to SDK/toolchain-controlled modules; ordinary user-authored modules MUST reject it.
+`declare host` and `declare builtin type` are reserved to SDK/toolchain-controlled modules; ordinary user-authored modules MUST reject them.
 
 ## 7. Declarations
 
 ### 7.1 Type declarations
 
 ```ebnf
-TypeDecl ::= StructDecl | ServiceDecl | ContractDecl | HostDecl | ErrorDecl | EnumDecl
+TypeDecl ::= StructDecl | ServiceDecl | ContractDecl | HostDecl | BuiltinTypeDecl | ErrorDecl | EnumDecl
 StructDecl ::= 'declare' 'struct' Identifier '(' StructFieldList? ')' (StructMethodBody | ';')
 ServiceDecl ::= 'declare' 'service' Identifier ServiceBody
 ContractDecl ::= 'declare' 'contract' Identifier ContractBody
 HostDecl ::= 'declare' 'host' Identifier HostBody
+BuiltinTypeDecl ::= AttrList? 'declare' 'builtin' 'type' Identifier '(' BuiltinFieldList? ')' BuiltinTypeBody
 ErrorDecl ::= 'declare' 'error' Identifier ErrorBody
 EnumDecl ::= 'declare' 'enum' Identifier '(' EnumCaseDecl (',' EnumCaseDecl)* ','? ')' ';'
 StructFieldList ::= StructFieldDecl (',' StructFieldDecl)* ','?
 StructFieldDecl ::= StructFieldAccess? Identifier ':' TypeRef
 StructFieldAccess ::= 'pub' MutOpt
+BuiltinFieldList ::= BuiltinFieldDecl (',' BuiltinFieldDecl)* ','?
+BuiltinFieldDecl ::= AttrList? BuiltinFieldAccess? Identifier ':' TypeRef
+BuiltinFieldAccess ::= 'pub'
 MutOpt ::= 'mut'?
 StructMethodBody ::= '{' StructMemberDecl* '}'
 StructMemberDecl ::= StructMethodDecl | StructCtorDecl
 StructMethodDecl ::= 'fn' Identifier ParamList ReturnAnn? Block
 StructCtorDecl ::= 'ctor' Identifier ParamList Block
 ContractBody ::= '{' FnSigDecl* '}'
+BuiltinTypeBody ::= '{' FnSigDecl* '}'
 ErrorBody ::= '{' ErrorCaseDecl+ '}'
 FieldDecl ::= Identifier ':' TypeRef ';'
 FnSigDecl ::= AttrList? 'fn' Identifier ParamList ReturnAnn? ';'
@@ -313,6 +319,14 @@ Rules:
 - A host declaration body contains only function signatures and no bodies.
 - Host declarations are reserved to SDK/toolchain-controlled modules and MUST be rejected in ordinary user-authored modules.
 - Host declarations do not declare fields, `ctor`, or `implements` bodies.
+- `declare builtin type Name(...) { ... }` declares a reserved SDK/toolchain builtin type shell with field-like projection metadata in the header and signature-only VM-owned member surfaces in the body.
+- A builtin type declaration body contains only function signatures and no bodies.
+- Builtin type declarations are reserved to SDK/toolchain-controlled modules and MUST be rejected in ordinary user-authored modules.
+- Builtin type declarations do not declare `ctor`, executable methods, or `implements` bodies.
+- Builtin type field entries are projection declarations, not ordinary struct storage fields.
+- Builtin type field entries may carry attributes where another specification explicitly permits them.
+- Builtin type field entries permit `pub` but do not permit `mut`.
+- Builtin method signatures MAY carry reserved VM-owned metadata such as `IntrinsicCall(...)`.
 - `declare error` bodies contain only error case labels.
 - `declare enum` uses a parenthesized case list and ends with `;`.
 - Error case labels in the same `declare error` body must be unique.
@@ -407,15 +421,18 @@ Rules:
 ### 7.6 Top-level constants
 
 ```ebnf
-ConstDecl ::= 'declare' 'const' Identifier ':' TypeRef '=' Expr ';'
+ConstDecl ::= AttrList? 'declare' 'const' Identifier ':' TypeRef ConstInitOpt ';'
+ConstInitOpt ::= ('=' Expr)?
 ```
 
 Rules:
 
 - Top-level constants MUST use `declare const`.
 - `declare const` is a declaration and may be exported through `mod.barrel`.
-- A `declare const` initializer MUST be a constant expression as defined by static semantics.
+- A `declare const` initializer is required unless another specification explicitly permits a reserved declaration-only shell such as builtin constant metadata.
+- A `declare const` initializer, when present, MUST be a constant expression as defined by static semantics.
 - `declare const` values are compile-time constants, not runtime-initialized module storage.
+- A reserved top-level builtin constant shell MAY use attributes such as `BuiltinConst(...)` and omit the initializer when another specification explicitly defines VM-owned materialization.
 
 ## 8. Type syntax
 
diff --git a/docs/specs/pbs/4. Static Semantics Specification.md b/docs/specs/pbs/4. Static Semantics Specification.md
index 78ad9bc0..3b5b7423 100644
--- a/docs/specs/pbs/4. Static Semantics Specification.md	
+++ b/docs/specs/pbs/4. Static Semantics Specification.md	
@@ -38,7 +38,7 @@ PBS distinguishes at least:
 
 Rules:
 
-- `declare struct`, `declare service`, `declare contract`, `declare error`, `declare enum`, and `declare callback` introduce names in the type namespace.
+- `declare struct`, `declare service`, `declare contract`, `declare error`, `declare enum`, `declare callback`, and `declare builtin type` introduce names in the type namespace.
 - `declare host` introduces names in the host-owner namespace.
 - `let`, parameters, and `declare const` introduce names in the value namespace.
 - `declare service Name` also introduces the canonical singleton value `Name` in the value namespace.
@@ -46,6 +46,7 @@ Rules:
 - `fn` declarations are not first-class values in v1 core and therefore do not become ordinary value expressions.
 - `bind(...)` is a callback-formation construct, not a general function-value construct.
 - `declare host` declarations are reserved to SDK/toolchain-controlled modules and are not formable in ordinary user-authored PBS source.
+- `declare builtin type` declarations are reserved to SDK/toolchain-controlled modules and are not formable in ordinary user-authored PBS source.
 - A host owner name is not an ordinary value expression in v1 core; it is used only as a qualified host-call owner.
 - The builtin simple types `int`, `float`, `bool`, and `str` are always present in the type namespace.
 - Builtin simple types are resolved without import or declaration.
@@ -61,11 +62,16 @@ Rules:
 - Attributes are not first-class values and are not reflectable in v1 core.
 - Attributes do not automatically survive into runtime or bytecode artifacts.
 - An attribute affects runtime artifacts only when another specification defines an explicit lowering for its semantic effect.
-- In v1 core, the only normative reserved attribute is `Host`.
+- In v1 core, the normative reserved attributes are `Host`, `BuiltinType`, `BuiltinConst`, `IntrinsicCall`, and `Slot`.
 - `Host` is valid only on a host method signature declared directly inside a reserved stdlib/interface-module `declare host` body.
 - `Host` is invalid on ordinary user-authored modules, top-level `fn`, struct methods, service methods, callbacks, contracts, and constants.
 - `Host` metadata is consumed by the compiler during host-binding lowering.
 - The `Host` attribute syntax itself is not exported as runtime metadata; instead, its canonical identity participates in PBX host-binding emission as defined by the Host ABI Binding specification.
+- `BuiltinType` is valid only on a reserved top-level `declare builtin type` declaration.
+- `BuiltinConst` is valid only on a reserved top-level `declare const` declaration that omits an initializer.
+- `IntrinsicCall` is valid only on a method signature declared directly inside a reserved `declare builtin type` body.
+- `Slot` is valid only on a field declaration in the header of a reserved `declare builtin type`.
+- Builtin metadata is consumed by the compiler during VM-owned builtin and intrinsic lowering rather than by host-binding lowering.
 
 ### 2.4 Tuple shapes
 
@@ -127,7 +133,8 @@ The following constructs are callable in v1 core:
 - contract values,
 - callback values,
 - service methods,
-- host methods on declared host owners.
+- host methods on declared host owners,
+- builtin intrinsic methods on declared builtin types.
 
 Rules:
 
@@ -137,6 +144,7 @@ Rules:
 - A callback declaration defines a nominal callable type with exactly one input/output tuple shape.
 - A service method is identified by `(service name, method name, input tuple shape, output tuple shape)`.
 - A host method is identified by `(host owner name, method name, input tuple shape, output tuple shape)` within the PBS declaration surface.
+- A builtin intrinsic method is identified within PBS declaration surface by `(builtin type name, method name, input tuple shape, output tuple shape)` and lowers further by canonical builtin/intrinsic metadata.
 - A top-level `fn` is identified by `(name, input tuple shape, output tuple shape)`.
 - A callback value is identified at the type level by its declared callback type and signature.
 - Contract signatures and barrel signatures must preserve the same callable shape.
@@ -166,9 +174,25 @@ Rules:
 - `Host.version` MUST be a positive integer literal.
 - Two host methods in the same resolved stdlib environment MUST NOT lower to the same canonical `(module, name, version)` unless they denote the same host method declaration after project/module resolution.
 - A `declare const` declaration must include an explicit type annotation.
-- A `declare const` initializer must be a constant expression.
+- A `declare const` declaration without `BuiltinConst` metadata must include an initializer.
+- A `declare const` declaration with `BuiltinConst` metadata must omit the initializer.
+- A non-builtin `declare const` initializer must be a constant expression.
 - `declare const` dependency resolution is module-wide and must not depend on source-file processing order.
 - `declare const` dependencies must form an acyclic graph.
+- A `BuiltinType` attribute MUST declare exactly the named arguments `name` and `version`.
+- `BuiltinType.name` MUST be a non-empty string literal.
+- `BuiltinType.version` MUST be a positive integer literal.
+- Two builtin type declarations in the same resolved stdlib environment MUST NOT lower to the same canonical `(name, version)` unless they denote the same builtin declaration after project/module resolution.
+- A builtin field type must be builtin-layout-admissible as defined by the builtin/intrinsics specification.
+- A builtin field `Slot` attribute, when present, MUST declare a non-negative integer literal and must match the declaration's canonical flattened layout.
+- `IntrinsicCall` MUST declare exactly the named argument `name` and MAY additionally declare `version`.
+- `IntrinsicCall.name` MUST be a non-empty string literal.
+- `IntrinsicCall.version`, when present, MUST be a positive integer literal.
+- Two builtin methods in the same canonical builtin owner/version line MUST NOT lower to the same canonical intrinsic `(owner, name, version)` unless they denote the same builtin method declaration after project/module resolution.
+- `BuiltinConst` MUST declare exactly the named arguments `target`, `name`, and `version`.
+- `BuiltinConst.target` and `BuiltinConst.name` MUST be non-empty string literals.
+- `BuiltinConst.version` MUST be a positive integer literal.
+- Two builtin constant declarations in the same resolved stdlib environment MUST NOT lower to the same canonical `(target, name, version)` unless they denote the same builtin constant declaration after project/module resolution.
 
 ### 3.4 Constant expressions
 
@@ -176,8 +200,8 @@ PBS core v1 restricts top-level constant evaluation to a deterministic compile-t
 
 Rules:
 
-- A `declare const` initializer is evaluated at compile time.
-- A `declare const` may depend only on previously resolved visible `declare const` declarations and enum case values.
+- A non-builtin `declare const` initializer is evaluated at compile time.
+- A non-builtin `declare const` may depend only on previously resolved visible `declare const` declarations and enum case values.
 - Cross-file constant resolution within a module is defined by dependency analysis, not source-file order.
 - Constant evaluation fails if the dependency graph contains a cycle.
 - The allowed constant-expression forms in v1 core are:
@@ -189,7 +213,7 @@ Rules:
   - binary arithmetic operators over numeric constant expressions,
   - binary comparison operators over compatible constant expressions,
   - binary boolean operators over boolean constant expressions.
-- A `declare const` initializer must not use:
+- A non-builtin `declare const` initializer must not use:
   - callable application or call sugar,
   - `new`,
   - `bind(...)`,
@@ -198,7 +222,8 @@ Rules:
   - block expressions,
   - `if`, `switch`, `handle`, `else` extraction, or `!` result propagation,
   - method calls or member access except enum case paths.
-- The initializer type must be compatible with the declared `const` type.
+- For non-builtin `declare const`, the initializer type must be compatible with the declared `const` type.
+- A `BuiltinConst` declaration is not part of ordinary compile-time constant evaluation and lowers through VM-owned builtin constant materialization instead.
 - A `declare const` exported through `mod.barrel` may be imported from another module only through ordinary module import rules.
 - A `declare const` does not introduce mutable runtime storage; implementations may inline, fold, or materialize it as an immutable constant as long as observable semantics remain unchanged.
 
@@ -500,10 +525,13 @@ Rules:
 - `HostName.method` is a valid method-call target when `HostName` resolves to a visible declared host owner whose body declares method `method`.
 - `TypeName.ctorName` is not a general member access surface; named constructors are entered only through `new TypeName.ctorName(...)`.
 - `expr.method` is a valid method-call target when the static type of `expr` is a contract value whose contract declares method `method`.
-- Bare extraction of a struct, service, host, or contract method as a value is invalid in v1 core because methods are not first-class.
+- Bare extraction of a struct, service, host, builtin, or contract method as a value is invalid in v1 core because methods are not first-class.
 - `expr.name` is valid when the static type of `expr` is a multi-slot named output tuple containing label `name`.
 - For named output tuples, the projected member type is the type of the corresponding output slot.
 - Projection is label-based, not position-based.
+- `expr.name` is valid when the static type of `expr` is a builtin type declaring projection field `name`.
+- For builtin projection fields, the projected member type is the declared builtin field type.
+- `expr.method` is a valid method-call target when the static type of `expr` is a builtin type declaring intrinsic member `method`.
 - `expr.hasSome()` and `expr.hasNone()` are valid intrinsic method-call surfaces when the static type of `expr` is `optional<P>`.
 - `expr.hasSome()` and `expr.hasNone()` both have static type `bool`.
 - `expr.name()` and `expr.key()` are valid intrinsic method-call surfaces when the static type of `expr` is an enum type.
@@ -517,6 +545,8 @@ Rules:
 - Access to a missing service method is a compile-time error.
 - Access to a missing host method is a compile-time error.
 - Access to a missing contract method is a compile-time error.
+- Access to a missing builtin projection field is a compile-time error.
+- Access to a missing builtin intrinsic member is a compile-time error.
 - Member projection is not defined for single-slot collapsed carrier values.
 
 ### 3.13 Block expressions and function fallthrough
@@ -621,11 +651,33 @@ At minimum, deterministic static diagnostics are required for:
 - invalid host method declaration shape,
 - invalid attribute surface,
 - invalid `Host` attribute target,
+- invalid `BuiltinType` attribute target,
+- invalid `BuiltinConst` attribute target,
+- invalid `IntrinsicCall` attribute target,
+- invalid `Slot` attribute target,
 - duplicate `Host` attribute on one host method,
 - missing required `Host` attribute on a reserved host method,
 - malformed `Host(module=..., name=..., version=...)` argument set,
 - invalid empty `Host.module` or `Host.name`,
 - invalid non-positive `Host.version`,
+- invalid builtin declaration shape,
+- invalid builtin method declaration shape,
+- missing required `BuiltinType` attribute on a reserved builtin declaration,
+- malformed `BuiltinType(name=..., version=...)` argument set,
+- invalid empty `BuiltinType.name`,
+- invalid non-positive `BuiltinType.version`,
+- malformed `IntrinsicCall(name=..., version=...)` argument set,
+- invalid empty `IntrinsicCall.name`,
+- invalid non-positive `IntrinsicCall.version`,
+- malformed `BuiltinConst(target=..., name=..., version=...)` argument set,
+- invalid empty `BuiltinConst.target` or `BuiltinConst.name`,
+- invalid non-positive `BuiltinConst.version`,
+- invalid builtin field `Slot(...)`,
+- overlapping builtin field slot range,
+- builtin field type not builtin-layout-admissible,
+- duplicate canonical builtin type identity,
+- duplicate canonical builtin intrinsic identity,
+- duplicate canonical builtin constant identity,
 - invalid `ctor` declaration shape,
 - invalid `return` inside `ctor`,
 - incomplete field initialization on a completing `ctor` path,
@@ -672,6 +724,7 @@ At minimum, deterministic static diagnostics are required for:
 - invalid `optional void` type surface,
 - invalid reuse of a builtin simple type name for a user-authored type declaration,
 - missing explicit type annotation on `declare const`,
+- missing initializer on non-builtin `declare const`,
 - non-constant `declare const` initializer,
 - incompatible `declare const` initializer type,
 - cyclic dependency among `declare const` declarations,
@@ -698,7 +751,10 @@ At minimum, deterministic static diagnostics are required for:
 - member access on a missing service method,
 - member access on a missing host method,
 - member access on a missing contract method,
-- bare method extraction from a struct, service, host, or contract value,
+- member access on a missing builtin projection field,
+- member access on a missing builtin intrinsic member,
+- bare method extraction from a struct, service, host, builtin, or contract value,
 - member projection on a single-slot carrier value,
 - invalid optional intrinsic member call,
+- invalid builtin intrinsic member call,
 - member projection on a missing named output label.
diff --git a/docs/specs/pbs/6. VM-owned vs Host-backed.md b/docs/specs/pbs/6. VM-owned vs Host-backed.md
new file mode 100644
index 00000000..219884c0
--- /dev/null
+++ b/docs/specs/pbs/6. VM-owned vs Host-backed.md	
@@ -0,0 +1,377 @@
+# VM-owned vs Host-backed
+
+Status: Draft v1 (Temporary)
+Applies to: ownership classification of PBS-visible operations, runtime boundary selection, and the normative distinction between VM-defined semantics and host-provided services
+
+## 1. Purpose
+
+This document defines the normative distinction between:
+
+- VM-owned operations,
+- host-backed operations,
+- and user-defined program operations.
+
+Its purpose is to prevent semantic drift between:
+
+- builtin language behavior,
+- VM execution behavior,
+- host/platform integration,
+- and source-level surfaces that may look similar while belonging to different ownership domains.
+
+This document exists because PBS must distinguish at least three different kinds
+of callable behavior:
+
+- program-owned functions,
+- VM-owned intrinsic behavior,
+- host-backed services.
+
+Without this distinction, the language would conflate:
+
+- builtin semantics with syscalls,
+- source-level shells with runtime authority,
+- and VM contracts with host capability-gated services.
+
+## 2. Scope
+
+This document defines:
+
+- the ownership model for callable behavior visible to PBS programs,
+- the normative difference between VM-owned and host-backed operations,
+- the runtime boundary crossed by each operation category,
+- the relationship between ownership and lowering form,
+- the relationship between ownership and determinism,
+- the relationship between ownership and capability checks,
+- the relationship between ownership and loader resolution,
+- and the classification rule used to decide whether a surface belongs to the VM or to the host.
+
+This document does not define:
+
+- the full parser grammar for builtin declarations,
+- the full intrinsic registry binary format,
+- the final PBX section numbering for intrinsic metadata,
+- subsystem-specific host APIs such as GFX or AUDIO,
+- or the complete dynamic semantics of every builtin type.
+
+## 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. `1. Language Charter.md`
+4. `3. Core Syntax Specification.md`
+5. `4. Static Semantics Specification.md`
+6. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+7. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+8. This document
+
+If a rule here conflicts with higher-precedence authority, the higher-precedence
+authority wins.
+
+## 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`
+
+## 5. Core Ownership Model
+
+PBS distinguishes three ownership categories for callable behavior.
+
+### 5.1 Program-owned function
+
+A program-owned function is authored by the program and compiled from a PBS body.
+
+Properties:
+
+- semantic ownership belongs to the program,
+- execution stays inside the VM,
+- source definition includes an executable body,
+- runtime dispatch uses ordinary function-call machinery,
+- authority does not depend on host capability grants.
+
+### 5.2 VM-owned operation
+
+A VM-owned operation is part of the semantic contract of the PBS platform.
+
+Properties:
+
+- semantic ownership belongs to the VM platform,
+- execution stays inside the VM,
+- behavior is not defined by user-authored PBS bodies,
+- behavior is not resolved against host registries,
+- behavior is not granted or denied by host capabilities,
+- and behavior is expected to remain semantically canonical across conforming implementations.
+
+VM-owned operations include, at minimum:
+
+- intrinsic operations over builtin types,
+- compiler-recognized intrinsic method-call surfaces over core semantic forms,
+- and other future VM-defined semantic helpers explicitly designated by spec.
+
+### 5.3 Host-backed operation
+
+A host-backed operation is provided by the runtime environment outside the VM's
+closed semantic domain.
+
+Properties:
+
+- semantic authority belongs to the host platform,
+- execution crosses the VM-to-host boundary,
+- resolution uses canonical host identity,
+- loader validation and capability checks are required before execution,
+- and the final executable form is numeric host dispatch.
+
+Host-backed operations are the domain of `declare host`, PBX `SYSC`, loader
+resolution, and final `SYSCALL`.
+
+## 6. The Boundary Question
+
+The normative classification question is:
+
+```text
+Does this operation belong to the VM's semantic contract, or does it require a
+service owned by the external host platform?
+```
+
+Rules:
+
+- If the operation expresses builtin language or VM semantics, it is VM-owned.
+- If the operation requires host-provided authority, devices, or platform services, it is host-backed.
+- If the operation is implemented by ordinary source code in the current program, it is program-owned.
+
+Heuristic:
+
+- if the operation must still have a complete meaning in a host-minimal VM, it is VM-owned,
+- if the operation loses meaning without external platform service, it is host-backed.
+
+Examples:
+
+- `Vec2.dot(other)` is VM-owned,
+- `Color.rgb(r, g, b)` is VM-owned,
+- `optional.hasSome()` is VM-owned,
+- `enumValue.name()` is VM-owned,
+- `Gfx.draw_pixel(x, y, c)` is host-backed,
+- `Input.is_pressed(button)` is host-backed.
+
+## 7. Runtime Boundary and Resolution Model
+
+### 7.1 VM-owned operations
+
+VM-owned operations do not cross the host boundary.
+
+Rules:
+
+- they do not resolve through the host syscall registry,
+- they do not emit `SYSC`,
+- they do not require loader-side capability checks,
+- they are not represented by `declare host`,
+- and they execute through VM-owned machinery such as intrinsic dispatch or other VM-defined execution paths.
+
+### 7.2 Host-backed operations
+
+Host-backed operations cross the VM boundary and require host authority.
+
+Rules:
+
+- they resolve by canonical host identity `(module, name, version)`,
+- they are represented in source through reserved host-binding surfaces,
+- they emit PBX host-binding metadata,
+- they are validated against authoritative host metadata during load,
+- and they execute in final form through `SYSCALL`.
+
+## 8. Semantic Authority
+
+The semantic owner of an operation is the layer that defines its normative
+meaning.
+
+### 8.1 VM-owned semantic authority
+
+For VM-owned operations:
+
+- the VM platform defines the operation's meaning,
+- the frontend may expose shell declarations but does not define behavior,
+- the host runtime must not redefine the operation's language-level semantics,
+- and the HAL may consume produced values but must not own their semantic definition.
+
+### 8.2 Host-backed semantic authority
+
+For host-backed operations:
+
+- the host platform defines the authoritative service identity and ABI,
+- the frontend exposes a compile-time shell only,
+- the loader resolves the shell's canonical identity against the host registry,
+- and the VM executes only the numeric form after loader patching.
+
+## 9. Determinism and Environmental Dependence
+
+Determinism requirements differ by ownership category.
+
+### 9.1 VM-owned operations
+
+VM-owned operations must not derive meaning from host service behavior.
+
+Rules:
+
+- a VM-owned operation must not call the host as part of its semantic definition,
+- a VM-owned operation must not require host capability grants,
+- a VM-owned operation must not depend on wall-clock time unless a higher-precedence authority explicitly allows it,
+- a VM-owned operation must not depend on frontend-generated helper algorithms for its canonical behavior,
+- and the VM contract must be specific enough that conformance can test its behavior.
+
+This does not require every VM-owned operation to be mathematically pure.
+It does require the operation's meaning to be owned and specified by the VM
+contract rather than delegated to the host.
+
+### 9.2 Host-backed operations
+
+Host-backed operations may depend on host state, devices, permissions, or
+platform policy.
+
+Rules:
+
+- host-backed operations may be denied by capability policy,
+- host-backed operations may vary by platform implementation within their ABI contract,
+- and host-backed operations are not reclassified as VM-owned merely because the source surface resembles an ordinary method call.
+
+## 10. Artifact Implications
+
+Ownership classification determines artifact form.
+
+### 10.1 Program-owned function artifact direction
+
+Program-owned functions lower to ordinary program call machinery.
+
+### 10.2 VM-owned artifact direction
+
+VM-owned operations lower to VM-facing artifacts.
+
+Illustrative forms:
+
+- direct intrinsic ids such as `INTRINSIC <id>`,
+- temporary intrinsic declaration tables plus pre-resolution callsites,
+- or other VM-internal runtime forms explicitly defined by future spec.
+
+Rules:
+
+- VM-owned operations must not be encoded as host-binding metadata merely because they are not authored in user code,
+- and VM-owned operations must not require host registry lookup.
+
+### 10.3 Host-backed artifact direction
+
+Host-backed operations lower to host-facing artifacts.
+
+Rules:
+
+- host-backed operations emit host-binding declarations into `SYSC`,
+- host-backed callsites use `HOSTCALL <sysc_index>` before load,
+- the loader resolves and patches those callsites,
+- and final execution uses `SYSCALL <id>`.
+
+## 11. Source Surface Similarity Does Not Collapse Ownership
+
+Two source surfaces may look similar while belonging to different ownership
+domains.
+
+Examples:
+
+- `Vec2.length()` may be VM-owned,
+- `Gfx.clear(color)` may be host-backed,
+- `value.name()` over an enum may be VM-owned,
+- and `service.method()` may be program-owned or service-owned ordinary PBS behavior.
+
+Rules:
+
+- source-level method-call syntax does not determine ownership,
+- declaration shape does not determine ownership,
+- ownership is determined by semantic authority and runtime boundary,
+- and toolchain metadata must classify the operation explicitly where ambiguity could arise.
+
+## 12. Relationship to `declare host`
+
+`declare host` is reserved exclusively for host-backed surfaces.
+
+Rules:
+
+- `declare host` must not be reused to model VM-owned builtin semantics,
+- host attributes such as `Host(module, name, version)` must not be used to identify VM-owned intrinsic behavior,
+- and a source surface that represents VM-owned behavior must use VM-specific metadata and lowering rules.
+
+Rationale:
+
+- `declare host` communicates external service ownership,
+- host attributes communicate loader-facing canonical identity,
+- and reusing them for VM-owned behavior would incorrectly imply host resolution, capability gating, and host semantic authority.
+
+## 13. Relationship to Builtin Types and Intrinsics
+
+Builtin types are VM-facing semantic types.
+
+Rules:
+
+- builtin types are not host APIs,
+- builtin type operations that belong to the builtin domain are VM-owned,
+- builtin constants, projections, constructors, and intrinsic methods are classified by VM semantics rather than by host service ownership,
+- and builtin values may later be passed to host-backed operations without transferring semantic ownership of the type itself.
+
+Example:
+
+- `Color` is VM-owned as a semantic type,
+- `Color.rgb(...)` is VM-owned,
+- `Pixel` may contain `Color` in its builtin layout,
+- `Gfx.draw_pixel(x, y, c)` is host-backed even when `c` has a VM-owned builtin type.
+
+## 14. Relationship to `stdlib` and SDK Surfaces
+
+`stdlib` and SDK packaging expose compile-time surfaces.
+
+Rules:
+
+- SDK or stdlib shells may expose both VM-owned and host-backed surfaces,
+- shell placement alone does not determine runtime ownership,
+- the runtime-facing artifact contract must preserve the true ownership category,
+- and compile-time convenience must not collapse VM-owned and host-backed operations into the same runtime mechanism.
+
+## 15. Classification Checklist
+
+When introducing a new callable surface, the spec author or toolchain author
+must answer at least these questions:
+
+1. Who owns the semantic meaning of this operation?
+2. Does the operation require host-provided authority, devices, or policy?
+3. Must the loader resolve the operation against an external registry?
+4. Can the operation be denied by capabilities?
+5. Should the operation continue to exist with complete meaning in a host-minimal VM?
+6. Is the operation part of builtin language semantics rather than platform service integration?
+
+Classification rule:
+
+- If answers 2, 3, or 4 are yes, the operation is host-backed.
+- If answer 6 is yes and 2, 3, and 4 are no, the operation is VM-owned.
+- Otherwise the operation is program-owned unless another spec defines a distinct category.
+
+## 16. Conformance Expectations
+
+Conforming implementations must preserve the ownership boundary.
+
+Rules:
+
+- an implementation must not lower VM-owned builtin semantics through the host syscall pipeline,
+- an implementation must not treat host-backed operations as if they were VM-defined intrinsic semantics,
+- an implementation must preserve the loader-facing host-binding contract for host-backed surfaces,
+- and an implementation must preserve VM-facing semantic ownership for builtin and intrinsic operations.
+
+## 17. Current Decision Summary
+
+The current model is:
+
+1. Program-authored functions are program-owned and execute through ordinary call machinery.
+2. Builtin semantics and intrinsic behavior are VM-owned.
+3. External platform services are host-backed.
+4. VM-owned behavior must not be modeled as `declare host`.
+5. Host-backed behavior must continue to use canonical host identity, `SYSC`, loader resolution, and final `SYSCALL`.
+6. Ownership is determined by semantic authority and runtime boundary, not by source-level syntax resemblance.
diff --git a/docs/specs/pbs/6.1. Intrinsics and Builtin Types Specification.md b/docs/specs/pbs/6.1. Intrinsics and Builtin Types Specification.md
new file mode 100644
index 00000000..f3c6c688
--- /dev/null
+++ b/docs/specs/pbs/6.1. Intrinsics and Builtin Types Specification.md	
@@ -0,0 +1,555 @@
+# Intrinsics and Builtin Types Specification
+
+Status: Draft v1 (Temporary)
+Applies to: builtin type declarations, builtin constants, intrinsic member surfaces, builtin layout metadata, lowering direction, and artifact-facing intrinsic contracts
+
+## 1. Purpose
+
+This document defines the PBS-facing contract for:
+
+- VM-owned builtin types,
+- VM-owned intrinsic operations,
+- and source-level shells that expose those features to PBS programs.
+
+Its purpose is to let the frontend expose builtin semantic types such as
+`Vec2`, `Color`, and `Pixel` as first-class language types while preserving
+three invariants:
+
+- semantic ownership remains with the VM,
+- builtin values have canonical stack layout,
+- and builtin domain behavior does not drift into host bindings or frontend helper code.
+
+## 2. Scope
+
+This document defines:
+
+- the source-level shell model for `declare builtin type`,
+- the canonical metadata carried by builtin type declarations,
+- builtin constants declared through reserved metadata,
+- builtin field layout and projection rules,
+- admissible field types for builtin layouts,
+- intrinsic member metadata and owner inheritance,
+- lowering categories for builtin declarations and members,
+- and the runtime-facing artifact direction for intrinsic operations.
+
+This document does not define:
+
+- the full final parser grammar integration into `3. Core Syntax Specification.md`,
+- the final PBX section numbering for intrinsic declarations,
+- the full VM intrinsic registry binary format,
+- user-extensible builtin types,
+- or heap-backed builtin layouts.
+
+## 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. `1. Language Charter.md`
+4. `3. Core Syntax Specification.md`
+5. `4. Static Semantics Specification.md`
+6. `5. Manifest, Stdlib, and SDK Resolution Specification.md`
+7. `6.2. Host ABI Binding and Loader Resolution Specification.md`
+8. `6. VM-owned vs Host-backed.md`
+9. This document
+
+If a rule here conflicts with higher-precedence authority, the higher-precedence
+authority wins.
+
+## 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`
+- `6. VM-owned vs Host-backed.md`
+- `12. IR and Lowering Specification.md`
+- `15. Bytecode and PBX Mapping Specification.md`
+
+## 5. Core Model
+
+### 5.1 Builtin type
+
+A builtin type is a VM-owned semantic type whose language-visible identity is
+not authored by ordinary user code.
+
+Properties:
+
+- the type is first-class in the PBS type system,
+- the type has canonical layout metadata,
+- the type may expose field-like projection surfaces,
+- the type may expose intrinsic member-call surfaces,
+- and the type's semantic meaning is owned by the VM rather than by `stdlib`, SDK packaging, or the host.
+
+### 5.2 Builtin declaration shell
+
+`declare builtin type` is a reserved shell declaration.
+
+Properties:
+
+- it exists for binding, checking, lowering, and artifact emission,
+- it has no user-authored executable body,
+- and it does not transfer semantic ownership away from the VM registry.
+
+### 5.3 Builtin constant
+
+A builtin constant is a VM-owned named value exposed to source through a
+reserved top-level `declare const` shell carrying builtin metadata.
+
+### 5.4 Intrinsic operation
+
+An intrinsic operation is a VM-owned callable behavior with canonical
+definition in the VM contract.
+
+## 6. Reserved Surface Forms
+
+This document temporarily defines the intended source-level shell shape.
+Final parser integration belongs to `3. Core Syntax Specification.md`.
+
+### 6.1 Builtin type shell
+
+Illustrative form:
+
+```pbs
+[BuiltinType(name="vec2", version=1)]
+declare builtin type Vec2(
+    [Slot(0)] pub x: float,
+    [Slot(1)] pub y: float,
+) {
+    [IntrinsicCall(name="dot")]
+    fn dot(other: Vec2) -> float;
+
+    [IntrinsicCall(name="length")]
+    fn length() -> float;
+}
+```
+
+### 6.2 Builtin constant shell
+
+Illustrative form:
+
+```pbs
+[BuiltinConst(target="vec2", name="zero", version=1)]
+declare const ZERO: Vec2;
+```
+
+## 7. `BuiltinType` Metadata
+
+`BuiltinType` declares the canonical VM-facing identity of a builtin type.
+
+Required fields:
+
+- `name`
+- `version`
+
+Rules:
+
+- the declaration name after `declare builtin type` is the PBS-visible type name,
+- `BuiltinType.name` is the canonical VM identity name,
+- `BuiltinType.version` is the canonical semantic version of that builtin contract,
+- the VM identity name need not equal the PBS-visible type name,
+- and the pair `(name, version)` is the canonical builtin type identity in v1.
+
+Example:
+
+- source-visible name: `Vec2`
+- canonical builtin identity: `("vec2", 1)`
+
+## 8. Declaration Form and Structural Rules
+
+`declare builtin type` uses a field-list surface similar to nominal aggregate
+declarations.
+
+Rules:
+
+- `declare builtin type` is reserved to SDK/toolchain-controlled modules,
+- ordinary user-authored modules must reject it,
+- the declaration introduces a type name in the type namespace,
+- the parenthesized member list declares builtin field projections,
+- the body may contain signatures only,
+- the body must not contain executable PBS statements,
+- builtin members must not declare PBS bodies,
+- and builtin declarations must not be used to encode ordinary user-defined structs.
+
+This surface is intentionally shell-like.
+The declaration is not the implementation authority for builtin behavior.
+
+## 9. Builtin Fields Are Projections, Not Ordinary Storage Fields
+
+The field-like entries in a builtin declaration describe named projections over a
+canonical VM layout.
+
+Rules:
+
+- they are not ordinary user-defined struct fields,
+- their names are visible for projection syntax such as `value.x`,
+- they describe a canonical flattened layout order,
+- and their meaning is projection over VM-owned builtin value representation.
+
+Consequences:
+
+- a builtin field declaration does not imply ordinary mutability semantics,
+- a builtin field declaration does not imply that builtin values are structs,
+- and a builtin field declaration does not allow user code to provide storage-level implementation bodies.
+
+## 10. `Slot` Metadata
+
+`Slot(n)` identifies the starting flattened slot offset of a builtin field within
+the enclosing builtin layout.
+
+Rules:
+
+- `n` is zero-based,
+- `Slot(n)` refers to the starting slot offset after flattening nested builtin-layout-admissible fields,
+- slot offsets must be unique,
+- slot offsets must match the declaration's canonical flattened layout,
+- and overlapping slot ranges are invalid.
+
+`Slot` exists to make canonical layout explicit.
+Future grammar may allow offset inference by declaration order, but explicit slot
+metadata is valid and authoritative in this temporary contract.
+
+## 11. Builtin Layout Admissibility
+
+Builtin field types are restricted.
+
+A type is builtin-layout-admissible when it has:
+
+- fixed width in slots,
+- finite flattened layout,
+- stack-only representation in this feature set,
+- and canonical VM-owned layout metadata.
+
+In v1 temporary scope, builtin-layout-admissible types are:
+
+- predeclared builtin scalar types whose runtime contract defines fixed slot width,
+- and declared builtin types whose own layout is fixed, finite, and stack-only.
+
+The following are not builtin-layout-admissible unless a future spec explicitly
+changes the rule:
+
+- user-declared structs,
+- services,
+- contracts,
+- callbacks,
+- `optional`,
+- `result`,
+- and any type with runtime-variable or heap-defined width.
+
+## 12. Nested Builtin Layout and Flattening
+
+Builtin fields may refer to other builtin-layout-admissible types.
+
+Rules:
+
+- nested builtin field types flatten recursively into the enclosing layout,
+- the enclosing builtin layout is the concatenation of its fields' flattened layouts in slot order,
+- a nested field retains its nominal field identity for projection purposes,
+- and verifier-facing slot widths are computed from the fully flattened layout.
+
+Example:
+
+```pbs
+[BuiltinType(name="color", version=1)]
+declare builtin type Color(
+    [Slot(0)] pub raw: int,
+);
+
+[BuiltinType(name="pixel", version=1)]
+declare builtin type Pixel(
+    [Slot(0)] pub x: int,
+    [Slot(1)] pub y: int,
+    [Slot(2)] pub color: Color,
+);
+```
+
+Canonical semantic layout:
+
+```text
+Pixel -> [int, int, Color]
+```
+
+Canonical flattened slot layout:
+
+```text
+Pixel -> [int, int, int]
+```
+
+## 13. Member Categories
+
+Builtin members belong to one of the following semantic categories:
+
+1. projection surface,
+2. builtin constant surface,
+3. layout-only constructor or factory surface,
+4. intrinsic call surface.
+
+This document normatively defines projection, builtin constants, and intrinsic
+call surfaces.
+Layout-only constructors may be introduced by future syntax or by existing
+constructor lowering rules, but their implementation remains VM-facing rather
+than host-backed.
+
+## 14. `IntrinsicCall` Metadata
+
+`IntrinsicCall` identifies a VM-owned callable member over builtin semantics.
+
+Required fields:
+
+- `name`
+
+Optional fields:
+
+- `version`
+
+Rules:
+
+- `IntrinsicCall` is valid only on method signatures declared inside a `declare builtin type` body,
+- the enclosing `BuiltinType` provides the default intrinsic owner identity,
+- `IntrinsicCall.name` is the canonical intrinsic operation name within that owner,
+- if `IntrinsicCall.version` is omitted, it inherits the enclosing builtin type version,
+- if `IntrinsicCall.version` is present, it overrides only the operation version,
+- and `IntrinsicCall` must not be interpreted as host-binding metadata.
+
+Canonical intrinsic identity in v1 is:
+
+```text
+(owner, name, version)
+```
+
+where:
+
+- `owner` is inherited from `BuiltinType.name`,
+- `name` is taken from `IntrinsicCall.name`,
+- and `version` is inherited or overridden as above.
+
+Example:
+
+```pbs
+[BuiltinType(name="vec2", version=1)]
+declare builtin type Vec2(
+    [Slot(0)] pub x: float,
+    [Slot(1)] pub y: float,
+) {
+    [IntrinsicCall(name="dot")]
+    fn dot(other: Vec2) -> float;
+}
+```
+
+declares canonical intrinsic identity:
+
+```text
+("vec2", "dot", 1)
+```
+
+## 15. `BuiltinConst` Metadata
+
+`BuiltinConst` identifies a VM-owned named constant surface.
+
+Required fields:
+
+- `target`
+- `name`
+- `version`
+
+Rules:
+
+- `BuiltinConst` is valid only on reserved top-level `declare const` shells,
+- `target` identifies the canonical builtin owner name,
+- `name` identifies the canonical constant name within that builtin owner,
+- `version` identifies the constant contract version,
+- the declared PBS constant name is source-visible and may differ from the canonical constant name,
+- and builtin constants are VM-owned declarations, not host bindings.
+
+Example:
+
+```pbs
+[BuiltinConst(target="vec2", name="zero", version=1)]
+declare const ZERO: Vec2;
+```
+
+declares a source-visible constant `ZERO` whose canonical builtin constant
+identity is:
+
+```text
+("vec2", "zero", 1)
+```
+
+## 16. Static Semantics
+
+The following static rules apply.
+
+### 16.1 Namespace rules
+
+Rules:
+
+- `declare builtin type` introduces a nominal type name in the type namespace,
+- builtin type names participate in visibility and import rules like other reserved type declarations,
+- ordinary user-authored type declarations must not redeclare visible builtin type names in the same scope,
+- and builtin constants declared through `declare const` introduce names in the value namespace.
+
+### 16.2 Member lookup rules
+
+Rules:
+
+- `expr.field` is valid when `expr` has a builtin type declaring a projection field named `field`,
+- the projected type is the field's declared type,
+- `expr.method()` is valid when the builtin type declares a matching intrinsic member surface,
+- and missing builtin fields or members are compile-time errors.
+
+### 16.3 Body restrictions
+
+Rules:
+
+- builtin declarations have no executable member bodies,
+- builtin methods are signature-only shells,
+- builtin constants are declaration-only shells,
+- and ordinary user code must not implement builtin semantics in PBS bodies.
+
+## 17. Lowering Model
+
+Builtin shells guide lowering; they do not supply executable implementation.
+
+### 17.1 Projection lowering
+
+Projection over builtin fields lowers to canonical projection over flattened
+layout.
+
+Rules:
+
+- field projection does not imply host interaction,
+- field projection does not emit `SYSC`,
+- field projection may lower to direct stack projection, reshaping operations, or another VM-owned form,
+- and the projected semantics are determined by builtin layout metadata.
+
+### 17.2 Builtin constant lowering
+
+Builtin constants lower to VM-owned constant materialization.
+
+Rules:
+
+- builtin constants must not lower through host binding resolution,
+- builtin constants may lower to direct value materialization, VM-owned constant pool lookup, or intrinsic-like constant fetch,
+- and the canonical constant identity determines which VM-owned value is materialized.
+
+### 17.3 Intrinsic method lowering
+
+Intrinsic methods lower to VM-owned intrinsic call behavior.
+
+Rules:
+
+- intrinsic methods must not lower through `SYSC`,
+- intrinsic methods must not emit `HOSTCALL`,
+- intrinsic method identities lower from `(owner, name, version)` metadata,
+- and the runtime-facing call form is VM-facing rather than host-facing.
+
+## 18. Artifact Direction
+
+This feature requires a distinct intrinsic artifact path.
+
+Illustrative final executable form:
+
+```text
+INTRINSIC <id>
+```
+
+Illustrative optional pre-resolution form:
+
+```text
+INTRCALL <decl_index>
+```
+
+with declaration metadata carrying:
+
+```text
+(owner, name, version)
+```
+
+Rules:
+
+- implementations may emit final `INTRINSIC <id>` directly when intrinsic ids are stable for the targeted VM contract,
+- implementations may emit declaration-based intrinsic callsites when a preload resolution step is desired,
+- any such intrinsic declaration path remains VM-facing and must not reuse host-binding metadata,
+- and intrinsic artifacts are distinct from `SYSC`, `HOSTCALL`, and `SYSCALL`.
+
+## 19. Verifier Obligations
+
+The verifier must treat intrinsics and builtin layouts as first-class structural
+facts.
+
+Rules:
+
+- each builtin type has a known flattened slot width,
+- each intrinsic has known argument and result layouts,
+- verifier stack effects are computed from flattened layouts rather than only from source spellings,
+- and verifier reasoning must preserve nominal builtin type identity even when two builtin layouts occupy the same slot width.
+
+Example:
+
+```text
+Vec2.dot(Vec2, Vec2) -> float
+```
+
+If `Vec2` flattens to two float-width slots, the verifier-facing stack effect is:
+
+```text
+pop 4, push 1
+```
+
+## 20. Determinism and Ownership Rules
+
+Builtin and intrinsic semantics are VM-owned.
+
+Rules:
+
+- builtin operations must not rely on host registry resolution,
+- builtin operations must not require runtime capability grants,
+- builtin operations must not be specified merely as frontend helper code,
+- and builtin operations must remain within the VM-owned category defined by `6. VM-owned vs Host-backed.md`.
+
+## 21. Relationship to `stdlib` and SDK Packaging
+
+`stdlib` and SDK packaging may expose builtin declarations as compile-time
+surfaces.
+
+Rules:
+
+- packaging location does not make builtin semantics host-backed,
+- source modules may import builtin shells from reserved stdlib surfaces,
+- the shell remains descriptive rather than semantically authoritative,
+- and the VM contract remains the owner of builtin identities, layouts, constants, and intrinsic behavior.
+
+## 22. Deterministic Static Errors
+
+At minimum, a conforming implementation must reject:
+
+1. `declare builtin type` in an ordinary user-authored module,
+2. missing required `BuiltinType` metadata on a builtin declaration,
+3. duplicate builtin field names within one declaration,
+4. duplicate or overlapping slot assignments,
+5. builtin field types that are not builtin-layout-admissible,
+6. `IntrinsicCall` used outside a builtin declaration body,
+7. `BuiltinConst` used outside a reserved top-level `declare const` shell,
+8. duplicate canonical builtin type identities in the same compilation environment,
+9. duplicate intrinsic canonical identities within the same builtin owner and version line,
+10. mismatched declared field slot metadata versus flattened layout,
+11. executable member bodies inside builtin declarations,
+12. any lowering that routes VM-owned builtin operations through the host-binding pipeline.
+
+## 23. Current Decision Summary
+
+The current temporary contract is:
+
+1. Builtin types are VM-owned semantic types exposed through reserved shell declarations.
+2. `BuiltinType(name, version)` maps source-visible type names to canonical VM builtin identities.
+3. Builtin fields describe projection surfaces over canonical flattened layout.
+4. Builtin field types must be builtin-layout-admissible and stack-only in this feature set.
+5. Builtin types may contain other builtin-layout-admissible types, including nested builtin composition such as `Pixel` containing `Color`.
+6. `IntrinsicCall(name, version?)` identifies VM-owned intrinsic member behavior and inherits owner identity from the enclosing builtin type.
+7. `BuiltinConst(target, name, version)` exposes VM-owned builtin constants through reserved top-level `declare const` shells.
+8. Builtin projections, constants, and intrinsic calls must not lower through `SYSC`, `HOSTCALL`, or `SYSCALL`.
+9. Runtime-facing intrinsic artifacts are distinct from host-binding artifacts.
diff --git a/docs/specs/pbs/6. Host ABI Binding and Loader Resolution Specification.md b/docs/specs/pbs/6.2. Host ABI Binding and Loader Resolution Specification.md
similarity index 100%
rename from docs/specs/pbs/6. Host ABI Binding and Loader Resolution Specification.md
rename to docs/specs/pbs/6.2. Host ABI Binding and Loader Resolution Specification.md
diff --git a/docs/specs/pbs/9. Dynamic Semantics Specification.md b/docs/specs/pbs/9. Dynamic Semantics Specification.md
new file mode 100644
index 00000000..4d569c31
--- /dev/null
+++ b/docs/specs/pbs/9. Dynamic Semantics Specification.md	
@@ -0,0 +1,133 @@
+# PBS Dynamic Semantics Specification
+
+Status: Draft v0 (Skeleton)  
+Applies to: runtime-observable behavior of PBS core programs
+
+## 1. Purpose
+
+This document will define 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 trap propagation,
+- 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 is intended to define:
+
+- 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 is expected to be closed using decisions from:
+
+- `docs/agendas/Dynamic Semantics - Execution Model Agenda.md`
+- `docs/agendas/Dynamic Semantics - Effect Surfaces Agenda.md`
+- `docs/agendas/Heap Model - Agenda.md`
+- `docs/agendas/Memory and Lifetime - Agenda.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`.
+- `bind(context, fn_name)` evaluates the `context` expression once at bind time.
+- `switch` evaluates its selector expression once.
+- `optional T` function fallthrough yields `none`.
+- `result<E>` function fallthrough is a compile-time error.
+- `ok(...)` and `err(...)` are not ordinary first-class runtime constructors in v1 core.
+
+## 6. Initial Section Targets
+
+At minimum, the completed document should contain normative sections for:
+
+1. execution model and runtime state,
+2. evaluation order by construct,
+3. block execution and abrupt completion,
+4. runtime semantics of `optional`,
+5. runtime semantics of `result<E>`,
+6. runtime semantics of `apply`, call sugar, and callable categories,
+7. branching semantics for `if` and `switch`,
+8. traps, determinism, and host-call interaction.
+
+## 7. A Ver
+
+The following items remain to be closed in agenda discussion before this document can be considered complete.
+
+### 7.1 `Dynamic Semantics - Execution Model Agenda.md`
+
+- Exact observable execution model for PBS v1.
+- Normative evaluation order for receivers, callees, arguments, selectors, and nested `apply`.
+- Exact abrupt-completion model for `return`, `break`, `continue`, `!`, and trap propagation.
+- Deterministic safepoint interaction around host calls, allocation-heavy operations, and loop back-edges.
+
+### 7.2 `Dynamic Semantics - Effect Surfaces Agenda.md`
+
+- Runtime value model of `optional` and `result<E>`.
+- Eagerness and single-evaluation guarantees for `some(...)`, `else`, `handle`, and `!`.
+- Runtime artifact and cost model of `bind(context, fn_name)`.
+- Exact runtime boundary between explicit status values and true traps.
+
+### 7.3 `Heap Model - Agenda.md` and `Memory and Lifetime - Agenda.md`
+
+- Which dynamic-semantic costs are observable and later diagnosable.
+- Which constructs may allocate, copy, retain, or cross the host-memory boundary during ordinary execution.
+- Which memory and safepoint facts belong in this document versus `Memory and Lifetime Specification.md`.
+
+## 8. 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.
+
+## 9. Exit Criteria
+
+This document is ready to move beyond skeleton status only when:
+
+1. every runtime-observable core construct has a deterministic evaluation model,
+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 requiring agenda backfill,
+5. the document no longer depends on unresolved `A Ver` items for core v1 behavior.
diff --git a/docs/specs/pbs/TODO.md b/docs/specs/pbs/TODO.md
deleted file mode 100644
index 5d2bee40..00000000
--- a/docs/specs/pbs/TODO.md
+++ /dev/null
@@ -1,72 +0,0 @@
-# PBS Spec Approval TODO
-
-Status: Draft  
-Purpose: checklist curto para decidir se a spec da PBS pode ser aprovada para seguir agora
-
-## Blockers
-
-- [X] Fechar o gate de prontidao para implementacao definido no charter para o escopo atual.
-  Decisao: a aprovacao atual cobre apenas implementacao faseada de frontend (`parser`, `AST` e `binding` inicial).
-  Isso fecha o gate apenas para esse escopo limitado e nao reclassifica a PBS como pronta para implementacao completa.
-  Dynamic semantics, memory and lifetime, diagnostics, IR/lowering e conformance permanecem como trabalho aberto para fases posteriores.
-  Referencia: `1. Language Charter.md`, secao "Required Spec Set Before Implementation".
-
-- [X] Substituir o antigo modelo publico de `host fn` por `declare host` reservado a SDK/toolchain.
-  Resolvido no nivel de charter, sintaxe e semantica estatica: bindings canonicos de host nao sao authorados pelo usuario comum, e superficies SDK usam `declare host` reservado.
-  O contrato de PBX/load/runtime continua pendente para a futura Host ABI Binding specification.
-  Referencias: `1. Language Charter.md`, `2. Governance and Versioning.md`, `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`, `5. Manifest, Stdlib, and SDK Resolution Specification.md`.
-
-- [X] Fechar a spec normativa de manifest/module/package/stdlib.
-  Resolvido com o modelo normativo de `project` e `module`, enderecamento canonico `@project:path/to/module`, `stdlib` como ambiente efetivo do build, `@sdk:*` e `@core:*` como project spaces reservados, interface modules PBS-like e atributos reservados de compile time como `[Host(...)]`.
-  Referencias: `5. Manifest, Stdlib, and SDK Resolution Specification.md`, `6. Host ABI Binding and Loader Resolution Specification.md`.
-
-- [X] Fechar o modelo semantico de `service` no core v1.
-  Resolvido com `declare service` como singleton nominal por modulo, exportado via barrel, com metodos sem visibilidade independente e suporte a `implements Contract for Service using s`.
-  Referencias: `3. Core Syntax Specification.md`, secao de `ServiceDecl`; `4. Static Semantics Specification.md`, callable categories.
-
-- [X] Remover do core v1 ou especificar completamente as superficies que ja existem na gramatica mas ainda nao tem contrato suficiente.
-  Itens visiveis hoje: `BoundedLit`, `GenericType`, `IndexSuffix` (`[]`) e `declare const` top-level.
-  Se permanecerem no v1, precisam de semantica estatica/dinamica e diagnosticos claros.
-  Referencia: `3. Core Syntax Specification.md`.
-
-## Non-Blockers
-
-- [x] Corrigir exemplos invalidos ou inconsistentes na spec estatica.
-  Ha exemplos com `let` em escopo top-level para callbacks, mas top-level `let` e proibido pela sintaxe.
-  Isso nao bloqueia a direcao da linguagem, mas deve ser corrigido para evitar ambiguidade.
-  Referencias: `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`.
-
-- [x] Consolidar exemplos canonicos para overload por retorno, `optional`, `result`, `bind`, `apply` e `switch`.
-  A base conceitual esta boa; o ajuste aqui e editorial e de conformance, nao arquitetural.
-
-- [X] Decidir se a implementacao pode comecar em modo faseado.
-  Decisao tomada: permitir apenas parser/AST/binding inicial nesta etapa.
-  Nao liberar ainda lowering, linker, host integration ou runtime behavior final.
-
-## Pautas Dedicadas
-
-- [X] Abrir pauta dedicada para dynamic semantics + memory and lifetime.
-  Resolvido com uma pauta guarda-chuva de heap model e tres pautas filhas separando: modelo de execucao, superfices de efeito/controle e memory/lifetime.
-  Isso reduz o acoplamento da discussao e permite fechar semantica observavel antes de fixar as regras normativas de heap e lifetime.
-  Objetivo: fechar o modelo de execucao observavel, ordem de avaliacao, traps, efeitos sobre `optional`/`result`/`apply`/`bind`/`switch`, baseline GC, fronteira heap VM vs memoria do host e visibilidade de custo/alocacao.
-  Resultado esperado: material para futura `Dynamic Semantics Specification` e `Memory and Lifetime Specification`.
-  Referencias: `Heap Model - Agenda.md`, `Dynamic Semantics - Execution Model Agenda.md`, `Dynamic Semantics - Effect Surfaces Agenda.md`, `Memory and Lifetime - Agenda.md`.
-
-- [X] Abrir pauta dedicada para validar se a `Host ABI Binding and Loader Resolution Specification` atual ja satisfaz o gate da fase seguinte ou se ainda precisa deixar de ser "Temporary".
-  Decisao: suficiente para a proxima fase. O contrato atual de `declare host` -> metadata PBX -> loader -> syscall numerico ja esta estavel o bastante para nao bloquear a etapa posterior.
-  Os pontos ainda abertos sao endurecimentos de formato/integracao, nao lacunas do contrato semantico principal.
-  Referencias: `Host ABI Gate Validation Agenda.md`, `6. Host ABI Binding and Loader Resolution Specification.md`.
-
-- [ ] FUTURO: abrir pauta de backend.
-  Objetivo: tratar IR/lowering, linker, host integration, runtime behavior final e conformance somente depois de fechar o frontend e aparar as arestas da linguagem/spec.
-  Resultado esperado: backlog da etapa de backend com precondicoes claras.
-  Esta pauta nao bloqueia o frontend faseado atual.
-
-## Decision Rule
-
-Pode aprovar a PBS para seguir agora somente se a aprovacao significar:
-
-- seguir com parser/frontend parcial, ou
-- seguir com fechamento das specs faltantes antes de runtime/lowering/linking.
-
-Nao aprovar como spec fechada para implementacao completa enquanto houver blockers abertos.