diff --git a/docs/specs/pbs/specs/Prometeu VM Memory model.md b/docs/specs/pbs/specs/Prometeu VM Memory model.md
new file mode 100644
index 00000000..5fdf5a9d
--- /dev/null
+++ b/docs/specs/pbs/specs/Prometeu VM Memory model.md	
@@ -0,0 +1,359 @@
+# Prometeu VM Memory Model v0
+
+> **Status:** v0 (normative, implementer-facing)
+>
+> **Purpose:** define the runtime memory model required to execute PBS programs with stable bytecode.
+>
+> This specification describes the four memory regions and their interactions:
+>
+> 1. **Constant Pool** (read-only)
+> 2. **Stack** (SAFE)
+> 3. **Heap** (HIP storage bytes/slots)
+> 4. **Gate Pool** (HIP handles, RC, metadata)
+
+---
+
+## 1. Design Goals
+
+1. **Bytecode stability**: instruction meanings and data formats must remain stable across versions.
+2. **Deterministic behavior**: no tracing GC; reclamation is defined by reference counts and safe points.
+3. **Explicit costs**: HIP allocation and aliasing are explicit via gates.
+4. **PBS alignment**: SAFE vs HIP semantics match PBS model.
+
+---
+
+## 2. Memory Regions Overview
+
+### 2.1 Constant Pool (RO)
+
+A program-wide immutable pool containing:
+
+* integers, floats, bounded ints
+* strings
+* (optional in future) constant composite literals
+
+Properties:
+
+* read-only during execution
+* indexed by `ConstId`
+* VM bytecode uses `PUSH_CONST(ConstId)`
+
+---
+
+### 2.2 Stack (SAFE)
+
+The **stack** contains:
+
+* local variables (by slot)
+* operand stack values for instruction evaluation
+
+SAFE properties:
+
+* values are copied by value
+* no aliasing across variables unless the value is a gate handle
+* stack values are reclaimed automatically when frames unwind
+
+---
+
+### 2.3 Heap (HIP storage)
+
+The **heap** is a contiguous array of machine slots (e.g., `Value` slots), used only as **storage backing** for HIP objects.
+
+Heap properties:
+
+* heap cells are not directly addressable by bytecode
+* heap is accessed only via **Gate Pool resolution**
+
+The heap may implement:
+
+* bump allocation (v0)
+* free list (optional)
+* compaction is **not** required in v0
+
+---
+
+### 2.4 Gate Pool (HIP handles)
+
+The **gate pool** is the authoritative table mapping a small integer handle (`GateId`) to a storage object.
+
+Gate Pool entry (conceptual):
+
+```text
+GateEntry {
+  alive: bool,
+  base: HeapIndex,
+  slots: u32,
+
+  strong_rc: u32,
+  weak_rc: u32,          // optional in v0; may be reserved
+
+  type_id: TypeId,       // required for layout + debug
+  flags: GateFlags,
+}
+```
+
+Properties:
+
+* `GateId` is stable during the lifetime of an entry
+* `GateId` values may be reused only after an entry is fully reclaimed (v0 may choose to never reuse)
+* any invalid `GateId` access is a **runtime trap** (deterministic)
+
+---
+
+## 3. SAFE vs HIP
+
+### 3.1 SAFE
+
+SAFE is stack-only execution:
+
+* primitives
+* structs / arrays as **value copies**
+* temporaries
+
+SAFE values are always reclaimed by frame unwinding.
+
+### 3.2 HIP
+
+HIP is heap-backed storage:
+
+* storage objects allocated with `alloc`
+* accessed through **gates**
+* aliasing occurs by copying a gate handle
+
+HIP values are reclaimed by **reference counting**.
+
+---
+
+## 4. Value Representation
+
+### 4.1 Stack Values
+
+A VM `Value` type must minimally support:
+
+* `Int(i64)`
+* `Float(f64)`
+* `Bounded(u32)`
+* `Bool(bool)`
+* `String(ConstId)` or `StringRef(ConstId)` (strings live in const pool)
+* `Gate(GateId)`  ← **this is the only HIP pointer form in v0**
+* `Unit`
+
+**Rule:** any former `Ref` pointer type must be reinterpreted as `GateId`.
+
+---
+
+## 5. Allocation (`alloc`) and Gate Creation
+
+### 5.1 Concept
+
+PBS `alloc` creates:
+
+1. heap backing storage (N slots)
+2. a gate pool entry
+3. returns a gate handle onto the stack
+
+### 5.2 Required inputs
+
+Allocation must be shape-explicit:
+
+* `TypeId` describing the allocated storage type
+* `slots` describing the storage size
+
+### 5.3 Runtime steps (normative)
+
+On `ALLOC(type_id, slots)`:
+
+1. allocate `slots` contiguous heap cells
+2. create gate entry:
+
+    * `base = heap_index`
+    * `slots = slots`
+    * `strong_rc = 1`
+    * `type_id = type_id`
+3. push `Gate(gate_id)` to stack
+
+### 5.4 Example
+
+PBS:
+
+```pbs
+let v: Box<Vector> = box(Vector.ZERO);
+```
+
+Lowering conceptually:
+
+* compute value `Vector.ZERO` (SAFE)
+* `ALLOC(TypeId(Vector), slots=2)` → returns `Gate(g0)`
+* store the two fields into heap via `STORE_GATE_FIELD`
+
+---
+
+## 6. Gate Access (Read/Write)
+
+### 6.1 Access Principle
+
+Heap is never accessed directly.
+All reads/writes go through:
+
+1. gate validation
+2. gate → (base, slots)
+3. bounds check
+4. heap read/write
+
+### 6.2 Read / Peek
+
+`peek` copies from HIP storage to SAFE value.
+
+* no RC changes
+* no aliasing is created
+
+### 6.3 Borrow (read-only view)
+
+Borrow provides temporary read-only access.
+
+* runtime may enforce with a borrow stack (debug)
+* v0 may treat borrow as a checked read scope
+
+### 6.4 Mutate (mutable view)
+
+Mutate provides temporary mutable access.
+
+* v0 may treat mutate as:
+
+    * read into scratch (SAFE)
+    * write back on `EndMutate`
+
+Or (preferred later):
+
+* direct heap writes within a guarded scope
+
+---
+
+## 7. Reference Counting (RC)
+
+### 7.1 Strong RC
+
+Strong RC counts how many **live gate handles** exist.
+
+A `GateId` is considered live if it exists in:
+
+* a stack slot
+* a global slot
+* a heap storage cell (HIP) (future refinement)
+
+### 7.2 RC operations
+
+When copying a gate handle into a new location:
+
+* increment `strong_rc`
+
+When a gate handle is removed/overwritten:
+
+* decrement `strong_rc`
+
+**Rule:** RC updates are required for any VM instruction that:
+
+* assigns locals/globals
+* stores into heap cells
+* pops stack values
+
+### 7.3 Release and Reclamation
+
+When `strong_rc` reaches 0:
+
+* gate entry becomes **eligible for reclamation**
+* actual reclamation occurs at a **safe point**
+
+Safe points (v0):
+
+* end of frame
+* explicit `FRAME_SYNC` (if present)
+
+Reclamation:
+
+1. mark gate entry `alive = false`
+2. optionally add heap region to a free list
+3. gate id may be recycled (optional)
+
+**No tracing GC** is performed.
+
+---
+
+## 8. Weak Gates (Reserved / Optional)
+
+v0 may reserve the field `weak_rc` but does not require full weak semantics.
+
+If implemented:
+
+* weak handles do not keep storage alive
+* upgrading weak → strong requires a runtime check
+
+---
+
+## 9. Runtime Traps (Deterministic)
+
+The VM must trap deterministically on:
+
+* invalid `GateId`
+* accessing a dead gate
+* out-of-bounds offset
+* type mismatch in a typed store/load (if enforced)
+
+Traps must include:
+
+* opcode
+* span (if debug info present)
+* message
+
+---
+
+## 10. Examples
+
+### 10.1 Aliasing via gates
+
+```pbs
+let a: Box<Vector> = box(Vector.ZERO);
+let b: Box<Vector> = a; // copy handle, RC++
+
+mutate b {
+  it.x += 10;
+}
+
+let v: Vector = unbox(a); // observes mutation
+```
+
+Explanation:
+
+* `a` and `b` are `GateId` copies
+* mutation writes to the same heap storage
+* `unbox(a)` peeks/copies storage into SAFE value
+
+### 10.2 No HIP for strings
+
+```pbs
+let s: string = "hello";
+```
+
+* string literal lives in constant pool
+* `s` is a SAFE value referencing `ConstId`
+
+---
+
+## 11. Conformance Checklist
+
+A VM is conformant with this spec if:
+
+* it implements the four memory regions
+* `GateId` is the only HIP pointer form
+* `ALLOC(type_id, slots)` returns `GateId`
+* heap access is only via gate resolution
+* RC increments/decrements occur on gate copies/drops
+* reclamation happens only at safe points
+
+---
+
+## Appendix A — Implementation Notes (Non-normative)
+
+* Start with bump-alloc heap + never-reuse GateIds (simplest v0)
+* Add free list later
+* Add borrow/mutate enforcement later as debug-only checks