prometeu-runtime/docs/specs/pbs/PRs para Junie.md

PBS ⇄ VM Alignment — Junie PRs (HIP Semantics Hardening)

Purpose: fix semantic mismatches between the PBS frontend (Core IR) and the VM before any VM heap/gate implementation.

These PRs are surgical, mandatory, and non-creative. Junie must follow them exactly.

Context:

• PBS frontend is implemented and produces Core IR.
• Bytecode stability is a hard requirement.
• VM currently has stack + const pool; heap exists but is unused.
• HIP semantics (gates/storage) are currently incorrectly lowered.
• ir_vm is feature-frozen at the moment. we are going to validate only ir_core
• Lowering is the only place ir_core and ir_vm touch each other.
  • VM IR is never imported from Core IR.
  • Core IR never imports VM IR.

---

Global Rules (Read Before Any PR)

1. No new features. Only semantic correction.
2. No new VM opcodes yet. VM changes come later.
3. No fallback values (e.g. FunctionId(0)). Fail with diagnostics.
4. Every PR must include tests (golden or unit).
5. Core IR is the source of semantic truth.

---

PR-20 — Core IR: Make HIP Semantics Explicit (No Handle Loss)

Goal

Fix the Core IR so HIP operations never lose the destination gate.

Problem (Current Bug)

Current lowering evaluates a gate, reads storage, stores the result in a local, and later attempts to write back without having the gate anymore.

This violates PBS semantics: storage access must always be mediated by the original gate.

Required Changes

1. Extend Core IR instructions

Add explicit HIP instructions:

enum CoreInstr {
  // existing …

  Alloc { ty: TypeId, slots: u32 },

  BeginPeek   { gate: ValueId },
  BeginBorrow { gate: ValueId },
  BeginMutate { gate: ValueId },

  EndPeek,
  EndBorrow,
  EndMutate,
}

Rules:

• Begin* instructions do not consume the gate.
• Gate identity must remain available until the matching End*.

2. Remove any lowering that copies HIP storage into locals

• No ReadGate → SetLocal pattern.
• Storage views are not locals.

Tests (Mandatory)

• Golden Core IR test showing BeginMutate(gate) … EndMutate wrapping body
• Test asserting gate is still live at EndMutate

---

PR-21 — Distinguish peek, borrow, and mutate in Core IR

Goal

Restore the semantic distinction mandated by PBS.

Required Semantics

Operation	Effect
peek	Copy storage → stack value
borrow	Temporary read-only view
mutate	Temporary mutable view + commit

Required Changes

• Lower PBS peek → BeginPeek / EndPeek
• Lower PBS borrow → BeginBorrow / EndBorrow
• Lower PBS mutate → BeginMutate / EndMutate

These must not share the same lowering path.

Tests

• PBS snippet with all three operations
• Assert distinct Core IR instruction sequences

---

PR-22 — Make Allocation Shape Explicit in Core IR

Goal

Stop implicit / guessed heap layouts.

Required Changes

• Replace any shape-less Alloc with:

Alloc { ty: TypeId, slots: u32 }

Rules:

• TypeId comes from frontend type checking
• slots is derived deterministically (struct fields / array size)

Tests

• Allocating storage struct emits correct slots
• Allocating array emits correct slots

---

PR-23 — Eliminate Invalid Call Fallbacks

Goal

Prevent invalid bytecode generation.

Required Changes

• Remove all fallbacks to FunctionId(0) or equivalent

• On unresolved symbols during lowering:

  • Emit canonical diagnostic (E_RESOLVE_UNDEFINED or E_LOWER_UNSUPPORTED)
  • Abort lowering

Tests

• PBS program calling missing function → compile error
• No Core IR or VM IR emitted

---

PR-24 — Validate Contract Calls in Frontend (Arity + Types)

Goal

Move contract validation to compile time.

Required Changes

• During PBS type checking:

  • Validate argument count against contract signature
  • Validate argument types

• Lower only validated calls to HostCall

Tests

• Wrong arity → E_TYPE_MISMATCH
• Correct call lowers to Core IR HostCall

---

PR-25 — Core IR Invariants Test Suite

Goal

Lock in correct semantics before touching the VM.

Required Invariants

• Every Begin* has a matching End*
• Gate passed to Begin* is available at End*
• No storage writes without BeginMutate
• No silent fallbacks

Tests

• Property-style tests or golden IR assertions

---

STOP POINT

After PR-25:

• Core IR correctly represents PBS HIP semantics
• Lowering is deterministic and safe
• VM is still unchanged

Only after this point may VM PRs begin.

Any VM work before this is a hard rejection.

---

Instruction to Junie

If any rule in this document is unclear:

• Stop
• Add a failing test
• Document the ambiguity

Do not invent behavior.

This document is binding.