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):

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:

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

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

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