prometeu-runtime/docs/specs/pbs/Prometeu VM Memory model.md

# 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