pr 26
This commit is contained in:
parent
81453cde84
commit
91af0d6f98
@ -1,3 +1,13 @@
|
||||
//! # VM Intermediate Representation (ir_vm)
|
||||
//!
|
||||
//! This module defines the Intermediate Representation for the Prometeu VM.
|
||||
//!
|
||||
//! ## Memory Model
|
||||
//!
|
||||
//! * Heap is never directly addressable.
|
||||
//! * All HIP (Heap) access is mediated via Gate Pool resolution.
|
||||
//! * `Gate(GateId)` is the only HIP pointer form in `ir_vm`.
|
||||
|
||||
pub mod types;
|
||||
pub mod module;
|
||||
pub mod instr;
|
||||
@ -5,7 +15,9 @@ pub mod validate;
|
||||
|
||||
pub use instr::{Instruction, InstrKind, Label};
|
||||
pub use module::{Module, Function, Global, Param};
|
||||
pub use types::Type;
|
||||
pub use types::{Type, Value, GateId};
|
||||
// Note: ConstId and TypeId are not exported here to avoid conflict with ir_core::ids
|
||||
// until the crates are fully decoupled.
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
|
||||
@ -1,5 +1,28 @@
|
||||
use serde::{Deserialize, Serialize};
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
|
||||
#[serde(transparent)]
|
||||
pub struct GateId(pub u32);
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
|
||||
#[serde(transparent)]
|
||||
pub struct ConstId(pub u32);
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
|
||||
#[serde(transparent)]
|
||||
pub struct TypeId(pub u32);
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
|
||||
pub enum Value {
|
||||
Int(i64),
|
||||
Float(f64),
|
||||
Bounded(u32),
|
||||
Bool(bool),
|
||||
Unit,
|
||||
Const(ConstId),
|
||||
Gate(GateId),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
|
||||
pub enum Type {
|
||||
Any,
|
||||
@ -14,3 +37,51 @@ pub enum Type {
|
||||
Function,
|
||||
Void,
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use std::collections::HashSet;
|
||||
|
||||
#[test]
|
||||
fn test_ids_implement_required_traits() {
|
||||
fn assert_copy<T: Copy>() {}
|
||||
fn assert_eq_hash<T: Eq + std::hash::Hash>() {}
|
||||
|
||||
assert_copy::<GateId>();
|
||||
assert_eq_hash::<GateId>();
|
||||
|
||||
assert_copy::<ConstId>();
|
||||
assert_eq_hash::<ConstId>();
|
||||
|
||||
assert_copy::<TypeId>();
|
||||
assert_eq_hash::<TypeId>();
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_gate_id_usage() {
|
||||
let id1 = GateId(1);
|
||||
let id2 = GateId(1);
|
||||
let id3 = GateId(2);
|
||||
|
||||
assert_eq!(id1, id2);
|
||||
assert_ne!(id1, id3);
|
||||
|
||||
let mut set = HashSet::new();
|
||||
set.insert(id1);
|
||||
assert!(set.contains(&id2));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_value_gate_exists_and_is_clonable() {
|
||||
let gate_id = GateId(42);
|
||||
let val = Value::Gate(gate_id);
|
||||
|
||||
let cloned_val = val.clone();
|
||||
if let Value::Gate(id) = cloned_val {
|
||||
assert_eq!(id, gate_id);
|
||||
} else {
|
||||
panic!("Expected Value::Gate");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,27 +1,27 @@
|
||||
# PBS ⇄ VM Alignment — Junie PRs (HIP Semantics Hardening)
|
||||
## Global Rules (Binding)
|
||||
|
||||
> **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**.
|
||||
1. **No semantic leakage**
|
||||
|
||||
> **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.
|
||||
* `ir_vm` must not encode PBS semantics (no `when`, `optional`, `result`, etc.).
|
||||
* `ir_core` must not encode VM execution details (no stack slots, no offsets-as-pointers).
|
||||
|
||||
2. **Feature freeze discipline**
|
||||
|
||||
* `ir_vm` is treated as a *stable ISA*.
|
||||
* Any change to `ir_vm` requires an explicit PR and review.
|
||||
|
||||
3. **No placeholders**
|
||||
|
||||
* No `LoadRef(0)`, no `Nop` as semantic stand-ins.
|
||||
* If something cannot be represented, the PR must stop and report it.
|
||||
|
||||
4. **No creativity**
|
||||
|
||||
* Implement exactly what is specified.
|
||||
* Do not add sugar, shortcuts, or inferred behavior.
|
||||
|
||||
5. **Tests are mandatory**
|
||||
|
||||
* Every PR must include tests validating the new surface.
|
||||
|
||||
---
|
||||
|
||||
## 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.**
|
||||
@ -1,17 +1,168 @@
|
||||
**Only after this point may VM PRs begin.**
|
||||
# PR-02 — Define `ir_vm` ISA v0 (Memory & Gates Only)
|
||||
|
||||
Any VM work before this is a hard rejection.
|
||||
### Goal
|
||||
|
||||
Define a minimal, PBS-compatible but PBS-agnostic VM instruction set.
|
||||
|
||||
### Required Instructions
|
||||
|
||||
#### Constant Pool
|
||||
|
||||
* `PushConst(ConstId)`
|
||||
|
||||
#### HIP Allocation (Deterministic)
|
||||
|
||||
* `Alloc { type_id: TypeId, slots: u32 }`
|
||||
|
||||
#### Gate-Based Heap Access
|
||||
|
||||
* `GateLoad { offset: u32 }`
|
||||
* `GateStore { offset: u32 }`
|
||||
|
||||
> All heap access must follow: gate validation → base+slots resolution → bounds check → read/write.
|
||||
|
||||
#### Scope Markers (Semantic Preservation)
|
||||
|
||||
* `GateBeginPeek` / `GateEndPeek`
|
||||
* `GateBeginBorrow` / `GateEndBorrow`
|
||||
* `GateBeginMutate` / `GateEndMutate`
|
||||
|
||||
> These may be runtime no-ops in v0 but must exist to preserve semantics and debug invariants.
|
||||
|
||||
#### Safe Point Hook
|
||||
|
||||
* `FrameSync` (optional but recommended)
|
||||
|
||||
### Non-goals
|
||||
|
||||
* No RC implementation
|
||||
* No VM execution logic
|
||||
|
||||
### Tests
|
||||
|
||||
* Unit tests ensuring the instruction enum is stable and cloneable
|
||||
* Snapshot or debug-format test to lock the ISA surface
|
||||
|
||||
---
|
||||
|
||||
## Instruction to Junie
|
||||
# PR-03 — Remove “Ref” Leakage from `ir_vm`
|
||||
|
||||
If any rule in this document is unclear:
|
||||
### Goal
|
||||
|
||||
* Stop
|
||||
* Add a failing test
|
||||
* Document the ambiguity
|
||||
Eliminate pointer-based mental models from the VM IR.
|
||||
|
||||
Do not invent behavior.
|
||||
### Required Changes
|
||||
|
||||
This document is binding.
|
||||
* Rename any existing `LoadRef` / `StoreRef` to:
|
||||
|
||||
* `LocalLoad { slot: u32 }`
|
||||
* `LocalStore { slot: u32 }`
|
||||
* Remove or rename any type named `Ref` that refers to HIP
|
||||
|
||||
**Hard rule:** the word `Ref` must never refer to HIP memory in `ir_vm`.
|
||||
|
||||
### Tests
|
||||
|
||||
* Grep-style or unit test ensuring no `Ref`-named HIP ops exist in `ir_vm`
|
||||
|
||||
---
|
||||
|
||||
# PR-04 — Update `core_to_vm` Lowering (Kill Placeholders)
|
||||
|
||||
### Goal
|
||||
|
||||
Make lowering the **only** integration point between Core IR and VM IR.
|
||||
|
||||
### Required Mapping
|
||||
|
||||
* `ir_core::Alloc { ty, slots }`
|
||||
→ `ir_vm::Alloc { type_id, slots }`
|
||||
|
||||
* `BeginPeek / Borrow / Mutate`
|
||||
→ `GateBegin*`
|
||||
|
||||
* `EndPeek / Borrow / Mutate`
|
||||
→ `GateEnd*`
|
||||
|
||||
**Forbidden:**
|
||||
|
||||
* `LoadRef(0)`
|
||||
* `Nop` as semantic replacement
|
||||
|
||||
### Tests
|
||||
|
||||
* Given a Core IR program with alloc + begin/end, VM IR must contain:
|
||||
|
||||
* shape-explicit `Alloc`
|
||||
* correctly paired gate begin/end
|
||||
* zero placeholders
|
||||
|
||||
---
|
||||
|
||||
# PR-05 — Gate-Aware Access Path (Choose One, Explicitly)
|
||||
|
||||
### Goal
|
||||
|
||||
Close the loop between Core IR access semantics and VM IR access execution.
|
||||
|
||||
### Choose One Approach (Explicit in PR Description)
|
||||
|
||||
#### Approach A (Preferred)
|
||||
|
||||
* Core IR expresses semantic access:
|
||||
|
||||
* `CoreGateLoadField(field_id)`
|
||||
* `CoreGateStoreField(field_id)`
|
||||
* Lowering resolves `field_id` → `offset`
|
||||
* VM IR emits `GateLoad/GateStore`
|
||||
|
||||
#### Approach B (Minimal)
|
||||
|
||||
* Core IR already carries `offset`
|
||||
* Lowering maps directly to `GateLoad/GateStore`
|
||||
|
||||
**Hard rule:** no direct heap access, no fake offsets.
|
||||
|
||||
### Tests
|
||||
|
||||
* Lowering emits correct offsets
|
||||
* Offset is visible in VM IR (not implicit)
|
||||
|
||||
---
|
||||
|
||||
# PR-06 — RC Hooks Documentation (No RC Yet)
|
||||
|
||||
### Goal
|
||||
|
||||
Prepare the VM for RC without implementing it yet.
|
||||
|
||||
### Required Changes
|
||||
|
||||
* Document which VM instructions are RC-sensitive:
|
||||
|
||||
* `LocalStore`
|
||||
* `GateStore`
|
||||
* stack pop / drop (if present)
|
||||
* frame end / `FrameSync` as safe points
|
||||
|
||||
* Document RC rules:
|
||||
|
||||
* retain on handle copy
|
||||
* release on overwrite/drop
|
||||
|
||||
### Tests
|
||||
|
||||
* Documentation test or unit assertion that the RC-sensitive list exists
|
||||
|
||||
---
|
||||
|
||||
## STOP POINT
|
||||
|
||||
After PR-06:
|
||||
|
||||
* `ir_core` and `ir_vm` are fully decoupled
|
||||
* Lowering is deterministic and placeholder-free
|
||||
* VM ISA v0 is defined and stable
|
||||
* VM runtime work may begin safely
|
||||
|
||||
**Any VM changes before this point must be rejected.**
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user