removed doc specs
This commit is contained in:
parent
98b899c380
commit
a04f462939
SSH Key Fingerprint:
SHA256:Z7dgqoglWwoK6j6u4QC87OveEq74WOhFN+gitsxtkf8
@ -1,359 +0,0 @@
|
||||
# PBS v0 Canonical Addenda
|
||||
|
||||
> **Purpose:** eliminate ambiguity for Junie and for golden tests.
|
||||
>
|
||||
> This document is **normative** for PBS Frontend v0 and complements:
|
||||
>
|
||||
> * **PBS Frontend Spec v0 — Implementer Edition**
|
||||
> * **Junie PR Plan**
|
||||
>
|
||||
> These addenda define:
|
||||
>
|
||||
> 1. operator precedence & associativity
|
||||
> 2. canonical AST JSON shape (v0)
|
||||
> 3. canonical diagnostic codes (v0)
|
||||
|
||||
---
|
||||
|
||||
## 1) Operator Precedence and Associativity (v0)
|
||||
|
||||
### 1.1 Guiding rule
|
||||
|
||||
PBS v0 prioritizes **minimal ambiguity** and **easy parsing**.
|
||||
|
||||
* Most operators are **left-associative**.
|
||||
* Assignment is **not** an expression in v0 (no `=` operator expressions).
|
||||
* Member access and indexing are not part of v0 surface syntax unless already defined elsewhere.
|
||||
|
||||
### 1.2 Precedence table
|
||||
|
||||
From **highest** to **lowest**:
|
||||
|
||||
1. **Primary**
|
||||
|
||||
* literals (`10`, `3.14`, `"text"`, `none`, `some(x)`, `ok(x)`, `err(e)`)
|
||||
* identifiers (`foo`)
|
||||
* parenthesized expression (`(expr)`)
|
||||
* block expression (`{ ... }`) (when allowed as `Expr`)
|
||||
|
||||
2. **Call** (left-associative)
|
||||
|
||||
* `callee(arg1, arg2, ...)`
|
||||
|
||||
3. **Unary prefix** (right-associative)
|
||||
|
||||
* `-expr`
|
||||
* `!expr`
|
||||
* `as` casts are **not unary**; see level 6.
|
||||
|
||||
4. **Multiplicative** (left-associative)
|
||||
|
||||
* `*`, `/`, `%`
|
||||
|
||||
5. **Additive** (left-associative)
|
||||
|
||||
* `+`, `-`
|
||||
|
||||
6. **Cast** (left-associative)
|
||||
|
||||
* `expr as Type`
|
||||
|
||||
7. **Comparison** (non-associative)
|
||||
|
||||
* `<`, `<=`, `>`, `>=`
|
||||
|
||||
8. **Equality** (non-associative)
|
||||
|
||||
* `==`, `!=`
|
||||
|
||||
9. **Logical AND** (left-associative)
|
||||
|
||||
* `&&`
|
||||
|
||||
10. **Logical OR** (left-associative)
|
||||
|
||||
* `||`
|
||||
|
||||
11. **Control expressions** (special)
|
||||
|
||||
* `if ... { ... } else { ... }` (expression form only if your v0 allows it; otherwise statement)
|
||||
* `when { ... }` (expression)
|
||||
|
||||
### 1.3 Non-associative rule
|
||||
|
||||
Comparison and equality are **non-associative**:
|
||||
|
||||
* `a < b < c` is an error
|
||||
* `a == b == c` is an error
|
||||
|
||||
Diagnostic: `E_PARSE_NON_ASSOC`.
|
||||
|
||||
### 1.4 Notes on `when`
|
||||
|
||||
`when` binds weaker than all binary operators.
|
||||
|
||||
Example:
|
||||
|
||||
```pbs
|
||||
let x = a + b when { ... };
|
||||
```
|
||||
|
||||
Parses as:
|
||||
|
||||
```
|
||||
let x = (a + b) when { ... };
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## 2) Canonical AST JSON (v0)
|
||||
|
||||
### 2.1 Canonicalization goals
|
||||
|
||||
Canonical AST JSON is used for:
|
||||
|
||||
* golden tests
|
||||
* frontend determinism validation
|
||||
* diff-friendly debugging
|
||||
|
||||
Rules:
|
||||
|
||||
* JSON keys are **stable** and **ordered** (when writing JSON)
|
||||
* All nodes include `kind` and `span`
|
||||
* Spans are byte offsets into the file content
|
||||
|
||||
### 2.2 Span encoding
|
||||
|
||||
```json
|
||||
{"file":"main.pbs","start":12,"end":18}
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
* `start` is inclusive
|
||||
* `end` is exclusive
|
||||
|
||||
### 2.3 Root
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "File",
|
||||
"span": {"file":"...","start":0,"end":123},
|
||||
"imports": [ ... ],
|
||||
"decls": [ ... ]
|
||||
}
|
||||
```
|
||||
|
||||
### 2.4 Import node
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "Import",
|
||||
"span": {"file":"...","start":0,"end":20},
|
||||
"spec": {"kind":"ImportSpec","path":["Foo","Bar"]},
|
||||
"from": "./lib.pbs"
|
||||
}
|
||||
```
|
||||
|
||||
`ImportSpec.path` is an array of identifiers.
|
||||
|
||||
### 2.5 Declarations
|
||||
|
||||
#### 2.5.1 Service
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "ServiceDecl",
|
||||
"span": {"file":"...","start":0,"end":50},
|
||||
"vis": "pub",
|
||||
"name": "Audio",
|
||||
"extends": null,
|
||||
"members": [ ... ]
|
||||
}
|
||||
```
|
||||
|
||||
A service member (method signature only in v0):
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "ServiceFnSig",
|
||||
"span": {"file":"...","start":0,"end":10},
|
||||
"name": "play",
|
||||
"params": [ {"name":"sound","ty": {"kind":"TypeName","name":"Sound"}} ],
|
||||
"ret": {"kind":"TypeName","name":"void"}
|
||||
}
|
||||
```
|
||||
|
||||
#### 2.5.2 Function
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "FnDecl",
|
||||
"span": {"file":"...","start":0,"end":80},
|
||||
"name": "main",
|
||||
"params": [],
|
||||
"ret": null,
|
||||
"else": null,
|
||||
"body": {"kind":"Block", ... }
|
||||
}
|
||||
```
|
||||
|
||||
#### 2.5.3 TypeDecl (struct/contract/error)
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "TypeDecl",
|
||||
"span": {"file":"...","start":0,"end":100},
|
||||
"vis": "pub",
|
||||
"typeKind": "struct",
|
||||
"name": "Vector",
|
||||
"body": {"kind":"TypeBody","members":[ ... ]}
|
||||
}
|
||||
```
|
||||
|
||||
### 2.6 Blocks and statements
|
||||
|
||||
Block:
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "Block",
|
||||
"span": {"file":"...","start":0,"end":20},
|
||||
"stmts": [ ... ],
|
||||
"tail": null
|
||||
}
|
||||
```
|
||||
|
||||
* `stmts` are statements.
|
||||
* `tail` is an optional final expression (only if your parser supports expression blocks).
|
||||
|
||||
Statement kinds (v0 minimum):
|
||||
|
||||
* `LetStmt`
|
||||
* `ExprStmt`
|
||||
* `ReturnStmt`
|
||||
|
||||
Let:
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "LetStmt",
|
||||
"span": {"file":"...","start":0,"end":20},
|
||||
"name": "x",
|
||||
"isMut": false,
|
||||
"ty": null,
|
||||
"init": {"kind":"IntLit", "value": 10, "span": ...}
|
||||
}
|
||||
```
|
||||
|
||||
Return:
|
||||
|
||||
```json
|
||||
{
|
||||
"kind": "ReturnStmt",
|
||||
"span": {"file":"...","start":0,"end":10},
|
||||
"expr": null
|
||||
}
|
||||
```
|
||||
|
||||
### 2.7 Expressions
|
||||
|
||||
All expressions include `kind` and `span`.
|
||||
|
||||
Minimal v0 expression node kinds:
|
||||
|
||||
* `IntLit` `{ value: i64 }`
|
||||
* `FloatLit` `{ value: f64 }`
|
||||
* `BoundedLit` `{ value: u32 }`
|
||||
* `StringLit` `{ value: string }`
|
||||
* `Ident` `{ name: string }`
|
||||
* `Call` `{ callee: Expr, args: Expr[] }`
|
||||
* `Unary` `{ op: "-"|"!", expr: Expr }`
|
||||
* `Binary` `{ op: string, left: Expr, right: Expr }`
|
||||
* `Cast` `{ expr: Expr, ty: TypeRef }`
|
||||
* `IfExpr` `{ cond: Expr, then: Block, els: Block }` (if expression is supported)
|
||||
* `WhenExpr` `{ arms: WhenArm[] }`
|
||||
|
||||
Type references:
|
||||
|
||||
```json
|
||||
{"kind":"TypeName","name":"int"}
|
||||
```
|
||||
|
||||
Generics:
|
||||
|
||||
```json
|
||||
{"kind":"TypeApp","base":"optional","args":[{"kind":"TypeName","name":"int"}]}
|
||||
```
|
||||
|
||||
### 2.8 Canonical JSON ordering
|
||||
|
||||
When writing AST JSON, always order fields as:
|
||||
|
||||
1. `kind`
|
||||
2. `span`
|
||||
3. semantic fields (stable order)
|
||||
|
||||
This makes diffs deterministic.
|
||||
|
||||
---
|
||||
|
||||
## 3) Diagnostic Codes (v0)
|
||||
|
||||
### 3.1 Diagnostic format
|
||||
|
||||
All diagnostics must be serializable to canonical JSON:
|
||||
|
||||
```json
|
||||
{
|
||||
"severity": "error",
|
||||
"code": "E_PARSE_UNEXPECTED_TOKEN",
|
||||
"message": "Unexpected token '}'",
|
||||
"span": {"file":"main.pbs","start":12,"end":13}
|
||||
}
|
||||
```
|
||||
|
||||
Severity is one of: `error`, `warning`.
|
||||
|
||||
### 3.2 Parse/Lex errors (E_PARSE_*)
|
||||
|
||||
* `E_LEX_INVALID_CHAR` — invalid character
|
||||
* `E_LEX_UNTERMINATED_STRING` — string literal not closed
|
||||
* `E_PARSE_UNEXPECTED_TOKEN` — token not expected in current context
|
||||
* `E_PARSE_EXPECTED_TOKEN` — missing required token
|
||||
* `E_PARSE_NON_ASSOC` — chained comparison/equality (non-associative)
|
||||
|
||||
### 3.3 Symbol/Resolve errors (E_RESOLVE_*)
|
||||
|
||||
* `E_RESOLVE_UNDEFINED` — undefined identifier
|
||||
* `E_RESOLVE_DUPLICATE_SYMBOL` — duplicate symbol in same namespace
|
||||
* `E_RESOLVE_NAMESPACE_COLLISION` — name exists in both type and value namespaces
|
||||
* `E_RESOLVE_VISIBILITY` — symbol not visible from this scope/module
|
||||
* `E_RESOLVE_INVALID_IMPORT` — import spec/path invalid
|
||||
|
||||
### 3.4 Type errors (E_TYPE_*)
|
||||
|
||||
* `E_TYPE_MISMATCH` — type mismatch
|
||||
* `E_TYPE_UNKNOWN_TYPE` — unknown type name
|
||||
* `E_TYPE_MUTABILITY` — mutability violation
|
||||
* `E_TYPE_RETURN_PATH` — not all paths return a value
|
||||
* `E_TYPE_INVALID_CAST` — invalid cast
|
||||
|
||||
### 3.5 Lowering errors (E_LOWER_*)
|
||||
|
||||
* `E_LOWER_UNSUPPORTED` — feature not supported in v0 lowering
|
||||
|
||||
### 3.6 Warnings (W_*)
|
||||
|
||||
Warnings are allowed in v0 but should be used sparingly.
|
||||
|
||||
* `W_UNUSED_LET` — unused local binding
|
||||
* `W_SHADOWING` — local shadows another binding
|
||||
|
||||
---
|
||||
|
||||
## Implementation Notes (Non-normative)
|
||||
|
||||
* Keep these addenda in `spec/` in the repo.
|
||||
* Use them to drive golden tests for AST and diagnostics.
|
||||
* If a future change alters canonical AST, bump a version and regenerate goldens deliberately.
|
||||
@ -1,321 +0,0 @@
|
||||
# Prometeu PBS v0 — Unified Project, Module, Linking & Execution Specification
|
||||
|
||||
> **Status:** Canonical / Replaces all previous module & linking specs
|
||||
>
|
||||
> This document **fully replaces**:
|
||||
>
|
||||
> * "PBS – Module and Linking Model"
|
||||
> * Any partial or implicit module/linking descriptions in earlier PBS documents
|
||||
>
|
||||
> After this document, there must be **no parallel or competing spec** describing project structure, modules, imports, or linking for PBS v0.
|
||||
|
||||
---
|
||||
|
||||
## 1. Purpose
|
||||
|
||||
This specification defines the **single authoritative model** for how a Prometeu PBS v0 program is:
|
||||
|
||||
1. Organized as a project
|
||||
2. Structured into modules
|
||||
3. Resolved and linked at compile time
|
||||
4. Emitted as one executable bytecode blob
|
||||
5. Loaded and executed by the Prometeu Virtual Machine
|
||||
|
||||
The primary objective is to **eliminate ambiguity** by enforcing a strict separation of responsibilities:
|
||||
|
||||
* **Compiler / Tooling**: all symbolic, structural, and linking work
|
||||
* **Runtime / VM**: verification and execution only
|
||||
|
||||
---
|
||||
|
||||
## 2. Core Principles
|
||||
|
||||
### 2.1 Compiler Finality Principle
|
||||
|
||||
All operations involving **names, symbols, structure, or intent** must be completed at compile time.
|
||||
|
||||
The VM **never**:
|
||||
|
||||
* Resolves symbols or names
|
||||
* Loads or links multiple modules
|
||||
* Applies relocations or fixups
|
||||
* Interprets imports or dependencies
|
||||
|
||||
### 2.2 Single-Blob Execution Principle
|
||||
|
||||
A PBS v0 program is executed as **one fully linked, self-contained bytecode blob**.
|
||||
|
||||
At runtime there is no concept of:
|
||||
|
||||
* Projects
|
||||
* Modules
|
||||
* Imports
|
||||
* Dependencies
|
||||
|
||||
These concepts exist **only in the compiler**.
|
||||
|
||||
---
|
||||
|
||||
## 3. Project Model
|
||||
|
||||
### 3.1 Project Root
|
||||
|
||||
A Prometeu project is defined by a directory containing:
|
||||
|
||||
* `prometeu.json` — project manifest (required)
|
||||
* One or more module directories
|
||||
|
||||
### 3.2 `prometeu.json` Manifest
|
||||
|
||||
The project manifest is mandatory and must define:
|
||||
|
||||
```json
|
||||
{
|
||||
"name": "example_project",
|
||||
"version": "0.1.0",
|
||||
"dependencies": {
|
||||
"core": "../core",
|
||||
"input": "../input"
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
#### Fields
|
||||
|
||||
* `name` (string, required)
|
||||
|
||||
* Canonical project identifier
|
||||
* `version` (string, required)
|
||||
* `dependencies` (map, optional)
|
||||
|
||||
* Key: dependency project name
|
||||
* Value: filesystem path or resolver hint
|
||||
|
||||
Dependency resolution is **purely a compiler concern**.
|
||||
|
||||
---
|
||||
|
||||
## 4. Module Model (Compile-Time Only)
|
||||
|
||||
### 4.1 Module Definition
|
||||
|
||||
* A module is a directory inside a project
|
||||
* Each module contains one or more `.pbs` source files
|
||||
|
||||
### 4.2 Visibility Rules
|
||||
|
||||
Visibility is enforced **exclusively at compile time**:
|
||||
|
||||
* `file`: visible only within the same source file
|
||||
* `mod`: visible within the same module
|
||||
* `pub`: visible to importing modules or projects
|
||||
|
||||
The VM has **zero awareness** of visibility.
|
||||
|
||||
---
|
||||
|
||||
## 5. Imports & Dependency Resolution
|
||||
|
||||
### 5.1 Import Syntax
|
||||
|
||||
Imports reference **projects and modules**, never files:
|
||||
|
||||
```
|
||||
import @core:math
|
||||
import @input:pad
|
||||
```
|
||||
|
||||
### 5.2 Resolution Pipeline
|
||||
|
||||
The compiler performs the following phases:
|
||||
|
||||
1. Project dependency graph resolution (via `prometeu.json`)
|
||||
2. Module discovery
|
||||
3. Symbol table construction
|
||||
4. Name and visibility resolution
|
||||
5. Type checking
|
||||
|
||||
Any failure aborts compilation and **never reaches the VM**.
|
||||
|
||||
---
|
||||
|
||||
## 6. Linking Model (Compiler Responsibility)
|
||||
|
||||
### 6.1 Link Stage
|
||||
|
||||
After semantic validation, the compiler executes a **mandatory link stage**.
|
||||
|
||||
The linker:
|
||||
|
||||
* Assigns final `func_id` indices
|
||||
* Assigns constant pool indices
|
||||
* Computes final `code_offset` and `code_len`
|
||||
* Resolves all jumps and calls
|
||||
* Merges all module bytecode into one contiguous code segment
|
||||
|
||||
### 6.2 Link Output Format
|
||||
|
||||
The output of linking is a **Linked PBS Program** with the following layout:
|
||||
|
||||
```text
|
||||
[ Header ]
|
||||
[ Constant Pool ]
|
||||
[ Function Table ]
|
||||
[ Code Segment ]
|
||||
```
|
||||
|
||||
All references are:
|
||||
|
||||
* Absolute
|
||||
* Final
|
||||
* Fully resolved
|
||||
|
||||
No relocations or fixups remain.
|
||||
|
||||
---
|
||||
|
||||
## 7. Runtime Execution Contract
|
||||
|
||||
### 7.1 VM Input Requirements
|
||||
|
||||
The Prometeu VM accepts **only linked PBS blobs**.
|
||||
|
||||
It assumes:
|
||||
|
||||
* All function references are valid
|
||||
* All jumps target instruction boundaries
|
||||
* No unresolved imports exist
|
||||
|
||||
### 7.2 VM Responsibilities
|
||||
|
||||
The VM is responsible for:
|
||||
|
||||
1. Loading the bytecode blob
|
||||
2. Structural and control-flow verification
|
||||
3. Stack discipline verification
|
||||
4. Deterministic execution
|
||||
|
||||
The VM **must not**:
|
||||
|
||||
* Perform linking
|
||||
* Resolve symbols
|
||||
* Modify code offsets
|
||||
* Load multiple modules
|
||||
|
||||
---
|
||||
|
||||
## 8. Errors and Runtime Traps
|
||||
|
||||
### 8.1 Compile-Time Errors
|
||||
|
||||
Handled exclusively by the compiler:
|
||||
|
||||
* Unresolved imports
|
||||
* Visibility violations
|
||||
* Type errors
|
||||
* Circular dependencies
|
||||
|
||||
These errors **never produce bytecode**.
|
||||
|
||||
### 8.2 Runtime Traps
|
||||
|
||||
Runtime traps represent **deterministic execution faults**, such as:
|
||||
|
||||
* Stack underflow
|
||||
* Invalid local access
|
||||
* Invalid syscall invocation
|
||||
* Explicit `TRAP` opcode
|
||||
|
||||
Traps are part of the **execution model**, not debugging.
|
||||
|
||||
---
|
||||
|
||||
## 9. Versioning and Scope
|
||||
|
||||
### 9.1 PBS v0 Guarantees
|
||||
|
||||
PBS v0 guarantees:
|
||||
|
||||
* Single-blob execution
|
||||
* No runtime linking
|
||||
* Deterministic behavior
|
||||
|
||||
### 9.2 Out of Scope for v0
|
||||
|
||||
The following are explicitly excluded from PBS v0:
|
||||
|
||||
* Dynamic module loading
|
||||
* Runtime imports
|
||||
* Hot reloading
|
||||
* Partial linking
|
||||
|
||||
---
|
||||
|
||||
## 10. Canonical Ownership Summary
|
||||
|
||||
| Concern | Owner |
|
||||
| ----------------- | ------------- |
|
||||
| Project structure | Compiler |
|
||||
| Dependencies | Compiler |
|
||||
| Modules & imports | Compiler |
|
||||
| Linking | Compiler |
|
||||
| Bytecode format | Bytecode spec |
|
||||
| Verification | VM |
|
||||
| Execution | VM |
|
||||
|
||||
> **Rule of thumb:**
|
||||
> If it requires names, symbols, or intent → compiler.
|
||||
> If it requires bytes, slots, or PCs → VM.
|
||||
|
||||
---
|
||||
|
||||
## 11. Final Note
|
||||
|
||||
After adoption of this document:
|
||||
|
||||
* Any existing or future document describing PBS modules or linking **must defer to this spec**
|
||||
* Any behavior conflicting with this spec is considered **non-compliant**
|
||||
* The Prometeu VM is formally defined as a **pure executor**, not a linker
|
||||
|
||||
---
|
||||
|
||||
## Addendum — `prometeu.json` and Dependency Management
|
||||
|
||||
This specification intentionally **does not standardize the full dependency resolution algorithm** for `prometeu.json`.
|
||||
|
||||
### Scope Clarification
|
||||
|
||||
* `prometeu.json` **defines project identity and declared dependencies only**.
|
||||
* **Dependency resolution, fetching, version selection, and conflict handling are responsibilities of the Prometeu Compiler**, not the VM and not the runtime bytecode format.
|
||||
* The Virtual Machine **never reads or interprets `prometeu.json`**.
|
||||
|
||||
### Compiler Responsibility
|
||||
|
||||
The compiler is responsible for:
|
||||
|
||||
* Resolving dependency sources (`path`, `git`, registry, etc.)
|
||||
* Selecting versions (exact, range, or `latest`)
|
||||
* Applying aliasing / renaming rules
|
||||
* Detecting conflicts and incompatibilities
|
||||
* Producing a **fully linked, closed-world Program Image**
|
||||
|
||||
After compilation and linking:
|
||||
|
||||
* All symbols are resolved
|
||||
* All function indices are fixed
|
||||
* All imports are flattened into the final bytecode image
|
||||
|
||||
The VM consumes **only the resulting bytecode blob** and associated metadata.
|
||||
|
||||
### Separate Specification
|
||||
|
||||
A **dedicated specification** will define:
|
||||
|
||||
* The complete schema of `prometeu.json`
|
||||
* Dependency version semantics
|
||||
* Resolution order and override rules
|
||||
* Tooling expectations (compiler, build system, CI)
|
||||
|
||||
This addendum exists to explicitly state the boundary:
|
||||
|
||||
> **`prometeu.json` is a compiler concern; dependency management is not part of the VM or bytecode execution model.**
|
||||
@ -1,268 +0,0 @@
|
||||
# Prometeu.json — Project Manifest Specification
|
||||
|
||||
## Status
|
||||
|
||||
Draft · Complementary specification to the PBS Linking & Module Model
|
||||
|
||||
## Purpose
|
||||
|
||||
`prometeu.json` is the **project manifest** for Prometeu-based software.
|
||||
|
||||
Its role is to:
|
||||
|
||||
* Identify a Prometeu project
|
||||
* Declare its dependencies
|
||||
* Provide **input metadata to the compiler and linker**
|
||||
|
||||
It is **not** consumed by the Virtual Machine.
|
||||
|
||||
---
|
||||
|
||||
## Design Principles
|
||||
|
||||
1. **Compiler-owned**
|
||||
|
||||
* Only the Prometeu Compiler reads `prometeu.json`.
|
||||
* The VM and runtime never see this file.
|
||||
|
||||
2. **Declarative, not procedural**
|
||||
|
||||
* The manifest declares *what* the project depends on, not *how* to resolve it.
|
||||
|
||||
3. **Closed-world output**
|
||||
|
||||
* Compilation + linking produce a single, fully resolved bytecode blob.
|
||||
|
||||
4. **Stable identity**
|
||||
|
||||
* Project identity is explicit and versioned.
|
||||
|
||||
---
|
||||
|
||||
## File Location
|
||||
|
||||
`prometeu.json` must be located at the **root of the project**.
|
||||
|
||||
---
|
||||
|
||||
## Top-level Structure
|
||||
|
||||
```json
|
||||
{
|
||||
"name": "my_project",
|
||||
"version": "0.1.0",
|
||||
"kind": "app",
|
||||
"dependencies": {
|
||||
"std": {
|
||||
"git": "https://github.com/prometeu/std",
|
||||
"version": ">=0.2.0"
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## Fields
|
||||
|
||||
### `name`
|
||||
|
||||
**Required**
|
||||
|
||||
* Logical name of the project
|
||||
* Used as the **default module namespace**
|
||||
|
||||
Rules:
|
||||
|
||||
* ASCII lowercase recommended
|
||||
* Must be unique within the dependency graph
|
||||
|
||||
Example:
|
||||
|
||||
```json
|
||||
"name": "sector_crawl"
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### `version`
|
||||
|
||||
**Required**
|
||||
|
||||
* Semantic version of the project
|
||||
* Used by the compiler for compatibility checks
|
||||
|
||||
Format:
|
||||
|
||||
```
|
||||
MAJOR.MINOR.PATCH
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### `kind`
|
||||
|
||||
**Optional** (default: `app`)
|
||||
|
||||
Defines how the project is treated by tooling.
|
||||
|
||||
Allowed values:
|
||||
|
||||
* `app` — executable program
|
||||
* `lib` — reusable module/library
|
||||
* `system` — firmware / system component
|
||||
|
||||
---
|
||||
|
||||
### `dependencies`
|
||||
|
||||
**Optional**
|
||||
|
||||
A map of **dependency aliases** to dependency specifications.
|
||||
|
||||
```json
|
||||
"dependencies": {
|
||||
"alias": { /* spec */ }
|
||||
}
|
||||
```
|
||||
|
||||
#### Alias semantics
|
||||
|
||||
* The **key** is the name by which the dependency is referenced **inside this project**.
|
||||
* It acts as a **rename / namespace alias**.
|
||||
|
||||
Example:
|
||||
|
||||
```json
|
||||
"dependencies": {
|
||||
"gfx": {
|
||||
"path": "../prometeu-gfx"
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
Internally, the dependency will be referenced as `gfx`, regardless of its original project name.
|
||||
|
||||
---
|
||||
|
||||
## Dependency Specification
|
||||
|
||||
Each dependency entry supports the following fields.
|
||||
|
||||
### `path`
|
||||
|
||||
Local filesystem dependency.
|
||||
|
||||
```json
|
||||
{
|
||||
"path": "../std"
|
||||
}
|
||||
```
|
||||
|
||||
Rules:
|
||||
|
||||
* Relative paths are resolved from the current `prometeu.json`
|
||||
* Absolute paths are allowed but discouraged
|
||||
|
||||
---
|
||||
|
||||
### `git`
|
||||
|
||||
Git-based dependency.
|
||||
|
||||
```json
|
||||
{
|
||||
"git": "https://github.com/prometeu/std",
|
||||
"version": "^0.3.0"
|
||||
}
|
||||
```
|
||||
|
||||
The compiler is responsible for:
|
||||
|
||||
* Cloning / fetching
|
||||
* Version selection
|
||||
* Caching
|
||||
|
||||
---
|
||||
|
||||
### `version`
|
||||
|
||||
Optional version constraint.
|
||||
|
||||
Examples:
|
||||
|
||||
* Exact:
|
||||
|
||||
```json
|
||||
"version": "0.3.1"
|
||||
```
|
||||
|
||||
* Range:
|
||||
|
||||
```json
|
||||
"version": ">=0.2.0 <1.0.0"
|
||||
```
|
||||
|
||||
* Latest:
|
||||
|
||||
```json
|
||||
"version": "latest"
|
||||
```
|
||||
|
||||
Semantics are defined by the compiler.
|
||||
|
||||
---
|
||||
|
||||
## Resolution Model (Compiler-side)
|
||||
|
||||
The compiler must:
|
||||
|
||||
1. Load root `prometeu.json`
|
||||
2. Resolve all dependencies recursively
|
||||
3. Apply aliasing rules
|
||||
4. Detect:
|
||||
|
||||
* Cycles
|
||||
* Version conflicts
|
||||
* Name collisions
|
||||
5. Produce a **flat module graph**
|
||||
6. Invoke the linker to generate a **single Program Image**
|
||||
|
||||
---
|
||||
|
||||
## Interaction with the Linker
|
||||
|
||||
* `prometeu.json` feeds the **module graph**
|
||||
* The linker:
|
||||
|
||||
* Assigns final function indices
|
||||
* Fixes imports/exports
|
||||
* Emits a closed bytecode image
|
||||
|
||||
After linking:
|
||||
|
||||
> No module boundaries or dependency information remain at runtime.
|
||||
|
||||
---
|
||||
|
||||
## Explicit Non-Goals
|
||||
|
||||
This specification does **not** define:
|
||||
|
||||
* Lockfiles
|
||||
* Registry formats
|
||||
* Caching strategies
|
||||
* Build profiles
|
||||
* Conditional dependencies
|
||||
|
||||
These may be added in future specs.
|
||||
|
||||
---
|
||||
|
||||
## Summary
|
||||
|
||||
* `prometeu.json` is the **single source of truth for project identity and dependencies**
|
||||
* Dependency management is **compiler-owned**
|
||||
* The VM executes **only fully linked bytecode**
|
||||
|
||||
This file completes the boundary between **project structure** and **runtime execution**.
|
||||
@ -1,446 +0,0 @@
|
||||
# Prometeu Base Script (PBS)
|
||||
|
||||
## Frontend Spec v0 — Implementer Edition
|
||||
|
||||
> **Normative specification for building a PBS frontend (lexer, parser, AST, resolver, typechecker) targeting the Prometeu Fantasy Console runtime.**
|
||||
>
|
||||
> This document is **not** a user guide.
|
||||
> It exists to make PBS *implementable*, *deterministic*, and *testable*.
|
||||
|
||||
---
|
||||
|
||||
## 0. Scope and Non‑Goals
|
||||
|
||||
### 0.1 Scope
|
||||
|
||||
This specification defines:
|
||||
|
||||
* lexical structure (tokens)
|
||||
* grammar and parsing rules
|
||||
* canonical AST shapes
|
||||
* frontend phases and their responsibilities
|
||||
* name resolution and visibility rules
|
||||
* type system rules
|
||||
* desugaring and lowering rules
|
||||
* diagnostic categories (errors vs warnings)
|
||||
* required guarantees for runtime integration
|
||||
|
||||
The goal is that **two independent frontends** built from this spec:
|
||||
|
||||
* accept the same programs
|
||||
* reject the same programs
|
||||
* produce equivalent ASTs
|
||||
* emit equivalent diagnostics
|
||||
|
||||
### 0.2 Non‑Goals
|
||||
|
||||
This spec does **not** define:
|
||||
|
||||
* runtime performance characteristics
|
||||
* bytecode layout
|
||||
* JIT or interpreter design
|
||||
* editor tooling or IDE features
|
||||
|
||||
Those are explicitly out of scope.
|
||||
|
||||
---
|
||||
|
||||
## 1. Frontend Pipeline Overview
|
||||
|
||||
A PBS frontend **must** be structured as the following pipeline:
|
||||
|
||||
```
|
||||
Source Text
|
||||
↓
|
||||
Lexer
|
||||
↓
|
||||
Parser
|
||||
↓
|
||||
Raw AST
|
||||
↓
|
||||
Symbol Collection
|
||||
↓
|
||||
Resolver
|
||||
↓
|
||||
Typed AST
|
||||
↓
|
||||
Desugaring / Lowering
|
||||
↓
|
||||
Runtime‑ready IR / AST
|
||||
```
|
||||
|
||||
Each stage has **strict responsibilities**.
|
||||
No stage may perform work assigned to a later stage.
|
||||
|
||||
---
|
||||
|
||||
## 2. Lexical Structure
|
||||
|
||||
### 2.1 Tokens
|
||||
|
||||
A PBS lexer must recognize at minimum the following token classes:
|
||||
|
||||
* identifiers
|
||||
* keywords
|
||||
* numeric literals
|
||||
* string literals
|
||||
* punctuation
|
||||
* operators
|
||||
* comments
|
||||
|
||||
Whitespace is insignificant except as a separator.
|
||||
|
||||
---
|
||||
|
||||
### 2.2 Keywords (Reserved)
|
||||
|
||||
The following keywords are **reserved** and may not be used as identifiers:
|
||||
|
||||
```
|
||||
import
|
||||
pub
|
||||
mod
|
||||
service
|
||||
fn
|
||||
let
|
||||
mut
|
||||
declare
|
||||
struct
|
||||
contract
|
||||
host
|
||||
error
|
||||
optional
|
||||
result
|
||||
some
|
||||
none
|
||||
ok
|
||||
err
|
||||
if
|
||||
else
|
||||
when
|
||||
for
|
||||
in
|
||||
return
|
||||
handle
|
||||
borrow
|
||||
mutate
|
||||
peek
|
||||
take
|
||||
alloc
|
||||
weak
|
||||
as
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### 2.3 Literals
|
||||
|
||||
#### Numeric Literals
|
||||
|
||||
* `int` — decimal digits
|
||||
* `float` — decimal with `.`
|
||||
* `bounded` — decimal digits suffixed with `b`
|
||||
|
||||
Examples:
|
||||
|
||||
```pbs
|
||||
10
|
||||
42
|
||||
3.14
|
||||
0b
|
||||
255b
|
||||
```
|
||||
|
||||
#### String Literals
|
||||
|
||||
* delimited by `"`
|
||||
* UTF‑8 encoded
|
||||
* immutable
|
||||
|
||||
---
|
||||
|
||||
### 2.4 Comments
|
||||
|
||||
* line comment: `// until end of line`
|
||||
* block comments are **not supported** in v0
|
||||
|
||||
---
|
||||
|
||||
## 3. Grammar (EBNF‑style)
|
||||
|
||||
> This grammar is **normative** but simplified for readability.
|
||||
> Implementers may refactor internally as long as semantics are preserved.
|
||||
|
||||
### 3.1 File Structure
|
||||
|
||||
```
|
||||
File ::= Import* TopLevelDecl*
|
||||
Import ::= 'import' ImportSpec 'from' StringLiteral
|
||||
TopLevelDecl::= TypeDecl | ServiceDecl | FnDecl
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### 3.2 Type Declarations
|
||||
|
||||
```
|
||||
TypeDecl ::= Visibility? 'declare' TypeKind Identifier TypeBody
|
||||
TypeKind ::= 'struct' | 'contract' | 'error'
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### 3.3 Services
|
||||
|
||||
```
|
||||
ServiceDecl ::= Visibility 'service' Identifier (':' Identifier)? Block
|
||||
```
|
||||
|
||||
Visibility is mandatory for services.
|
||||
|
||||
---
|
||||
|
||||
### 3.4 Functions
|
||||
|
||||
```
|
||||
FnDecl ::= Visibility? 'fn' Identifier ParamList ReturnType? ElseFallback? Block
|
||||
```
|
||||
|
||||
Top‑level `fn` are `mod` or `file-private` (default). They cannot be `pub`.
|
||||
|
||||
---
|
||||
|
||||
### 3.5 Expressions (Partial)
|
||||
|
||||
```
|
||||
Expr ::= Literal
|
||||
| Identifier
|
||||
| CallExpr
|
||||
| Block
|
||||
| IfExpr
|
||||
| WhenExpr
|
||||
| ForExpr
|
||||
| ReturnExpr
|
||||
```
|
||||
|
||||
Expression grammar is intentionally restricted in v0.
|
||||
|
||||
---
|
||||
|
||||
## 4. Canonical AST
|
||||
|
||||
The frontend **must** produce a canonical AST.
|
||||
|
||||
### 4.1 AST Invariants
|
||||
|
||||
* AST nodes are immutable after creation
|
||||
* Parent pointers are optional
|
||||
* Source spans must be preserved for diagnostics
|
||||
|
||||
---
|
||||
|
||||
### 4.2 Core Node Kinds
|
||||
|
||||
Minimal required node kinds:
|
||||
|
||||
* `FileNode`
|
||||
* `ImportNode`
|
||||
* `ServiceNode`
|
||||
* `FunctionNode`
|
||||
* `StructDeclNode`
|
||||
* `ContractDeclNode`
|
||||
* `BlockNode`
|
||||
* `LetNode`
|
||||
* `CallNode`
|
||||
* `IfNode`
|
||||
* `WhenNode`
|
||||
* `ForNode`
|
||||
* `ReturnNode`
|
||||
|
||||
Implementers may add internal nodes but must normalize before later phases.
|
||||
|
||||
---
|
||||
|
||||
## 5. Symbol Collection Phase
|
||||
|
||||
### 5.1 Purpose
|
||||
|
||||
Symbol Collection builds **module‑level symbol tables** without resolving bodies.
|
||||
|
||||
Collected symbols:
|
||||
|
||||
* `pub` and `mod` type declarations
|
||||
* `pub` and `mod` services
|
||||
|
||||
Excluded:
|
||||
|
||||
* function bodies
|
||||
* expressions
|
||||
* local bindings
|
||||
|
||||
---
|
||||
|
||||
### 5.2 Namespaces
|
||||
|
||||
PBS has **two namespaces**:
|
||||
|
||||
* Type namespace
|
||||
* Value namespace
|
||||
|
||||
Rules:
|
||||
|
||||
* A name may not exist in both namespaces
|
||||
* Violations are compile‑time errors
|
||||
|
||||
---
|
||||
|
||||
## 6. Resolver Phase
|
||||
|
||||
### 6.1 Responsibilities
|
||||
|
||||
Resolver must:
|
||||
|
||||
* resolve all identifiers
|
||||
* enforce visibility rules
|
||||
* bind references to symbols
|
||||
|
||||
Resolution order (per namespace):
|
||||
|
||||
1. local bindings
|
||||
2. file‑private declarations
|
||||
3. module symbols
|
||||
4. imported symbols
|
||||
|
||||
---
|
||||
|
||||
### 6.2 Visibility Rules (Normative)
|
||||
|
||||
* file‑private: visible only in the same file
|
||||
* `mod`: visible within the module
|
||||
* `pub`: visible across modules via import
|
||||
|
||||
Violations are errors.
|
||||
|
||||
---
|
||||
|
||||
## 7. Type Checking
|
||||
|
||||
### 7.1 Type Categories
|
||||
|
||||
Frontend must support:
|
||||
|
||||
* primitive types
|
||||
* struct value types
|
||||
* `optional<T>`
|
||||
* `result<T, E>`
|
||||
* gate‑backed types (opaque at frontend level)
|
||||
|
||||
---
|
||||
|
||||
### 7.2 Mutability Rules
|
||||
|
||||
* mutability belongs to bindings, not types
|
||||
* `mut` is part of binding metadata
|
||||
* mutability violations are compile‑time errors
|
||||
|
||||
---
|
||||
|
||||
### 7.3 Function Checking
|
||||
|
||||
Rules:
|
||||
|
||||
* all paths must return a value unless `else` fallback exists
|
||||
* `optional<T>` may implicitly return `none`
|
||||
* `result<T,E>` must return explicitly
|
||||
|
||||
---
|
||||
|
||||
## 8. Desugaring and Lowering
|
||||
|
||||
### 8.1 Purpose
|
||||
|
||||
Lowering transforms surface syntax into a minimal core language.
|
||||
|
||||
Examples:
|
||||
|
||||
* `take x.push(v)` → `mutate x as t { t.push(v) }`
|
||||
* `when` → conditional expression node
|
||||
* implicit `return none` for `optional<T>`
|
||||
|
||||
Lowered AST must contain **no syntactic sugar**.
|
||||
|
||||
---
|
||||
|
||||
## 9. Diagnostics Model
|
||||
|
||||
Diagnostics are first‑class frontend outputs.
|
||||
|
||||
### 9.1 Categories
|
||||
|
||||
* Error — compilation must fail
|
||||
* Warning — compilation may continue
|
||||
|
||||
---
|
||||
|
||||
### 9.2 Required Errors
|
||||
|
||||
Examples:
|
||||
|
||||
* unresolved identifier
|
||||
* visibility violation
|
||||
* type mismatch
|
||||
* mutability violation
|
||||
* invalid gate conversion
|
||||
|
||||
---
|
||||
|
||||
## 10. Runtime Interface Assumptions
|
||||
|
||||
Frontend assumes:
|
||||
|
||||
* host‑bound contracts map to runtime syscalls
|
||||
* allocation primitives exist (`alloc`)
|
||||
* reference counting is handled by runtime
|
||||
|
||||
Frontend must **not** assume GC or heap layout.
|
||||
|
||||
---
|
||||
|
||||
## 11. Determinism Guarantees
|
||||
|
||||
A valid PBS frontend **must guarantee**:
|
||||
|
||||
* deterministic parsing
|
||||
* deterministic name resolution
|
||||
* deterministic type checking
|
||||
* deterministic diagnostics
|
||||
|
||||
No frontend stage may depend on execution order or host state.
|
||||
|
||||
---
|
||||
|
||||
## 12. Conformance Criteria
|
||||
|
||||
A frontend is PBS‑v0‑conformant if:
|
||||
|
||||
* it implements all rules in this document
|
||||
* it produces canonical ASTs
|
||||
* it rejects all invalid programs defined herein
|
||||
|
||||
This document is the **source of truth** for PBS v0 frontend behavior.
|
||||
|
||||
---
|
||||
|
||||
## 13. Future Evolution (Non‑Normative)
|
||||
|
||||
Future versions may add:
|
||||
|
||||
* pattern matching
|
||||
* richer type inference
|
||||
* macros
|
||||
|
||||
No v0 frontend is required to support these.
|
||||
|
||||
---
|
||||
|
||||
## End of Spec
|
||||
@ -1,175 +0,0 @@
|
||||
# Runtime Traps v0 — Prometeu VM Specification
|
||||
|
||||
> **Status:** Proposed (requires explicit owner approval)
|
||||
>
|
||||
> **Scope:** Prometeu VM / PBS v0 execution model
|
||||
|
||||
---
|
||||
|
||||
## 1. Motivation
|
||||
|
||||
Prometeu aims to be a **deterministic, industrial-grade virtual machine**.
|
||||
To achieve this, execution errors that are:
|
||||
|
||||
* caused by **user programs**,
|
||||
* predictable by the execution model,
|
||||
* and recoverable at the tooling / host level,
|
||||
|
||||
must be **explicitly represented** and **ABI-stable**.
|
||||
|
||||
This specification introduces **Runtime Traps** as a *formal concept*, consolidating behavior that already existed implicitly in the VM.
|
||||
|
||||
---
|
||||
|
||||
## 2. Definition
|
||||
|
||||
A **Runtime Trap** is a **controlled interruption of program execution** caused by a semantic violation detected at runtime.
|
||||
|
||||
A trap:
|
||||
|
||||
* **terminates the current execution frame** (or program, depending on host policy)
|
||||
* **does not corrupt VM state**
|
||||
* **returns structured diagnostic information** (`TrapInfo`)
|
||||
* **is deterministic** for a given bytecode + state
|
||||
|
||||
A trap is **not**:
|
||||
|
||||
* a debugger breakpoint
|
||||
* undefined behavior
|
||||
* a VM panic
|
||||
* a verifier/load-time error
|
||||
|
||||
---
|
||||
|
||||
## 3. Trap vs Other Failure Modes
|
||||
|
||||
| Category | When | Recoverable | ABI-stable | Example |
|
||||
| ------------------ | ---------------------- | ----------- | ---------- | -------------------------------- |
|
||||
| **Verifier error** | Load-time | ❌ | ❌ | Stack underflow, bad CFG join |
|
||||
| **Runtime trap** | Execution | ✅ | ✅ | OOB access, invalid local |
|
||||
| **VM panic** | VM invariant violation | ❌ | ❌ | Handler returns wrong slot count |
|
||||
| **Breakpoint** | Debug only | ✅ | ❌ | Developer inspection |
|
||||
|
||||
---
|
||||
|
||||
## 4. Trap Information (`TrapInfo`)
|
||||
|
||||
All runtime traps must produce a `TrapInfo` structure with the following fields:
|
||||
|
||||
```text
|
||||
TrapInfo {
|
||||
code: u32, // ABI-stable trap code
|
||||
opcode: u16, // opcode that triggered the trap
|
||||
pc: u32, // program counter (relative to module)
|
||||
message: String, // human-readable explanation (non-ABI)
|
||||
}
|
||||
```
|
||||
|
||||
### ABI Guarantees
|
||||
|
||||
* `code`, `opcode`, and `pc` are ABI-relevant and stable
|
||||
* `message` is diagnostic only and may change
|
||||
|
||||
---
|
||||
|
||||
## 5. Standard Trap Codes (v0)
|
||||
|
||||
### 5.1 Memory & Bounds
|
||||
|
||||
| Code | Name | Meaning |
|
||||
| -------------------- | ------------- | ------------------------------ |
|
||||
| `TRAP_OOB` | Out of bounds | Access beyond allowed bounds |
|
||||
| `TRAP_INVALID_LOCAL` | Invalid local | Local slot index out of bounds |
|
||||
|
||||
### 5.2 Execution & Types
|
||||
|
||||
| Code | Name | Meaning |
|
||||
| ------------------------- | -------------------- | ------------------------------------------------------ |
|
||||
| `TRAP_ILLEGAL_INSTRUCTION`| Illegal instruction | Unknown/invalid opcode encountered |
|
||||
| `TRAP_TYPE` | Type violation | Type mismatch for operation or syscall argument types |
|
||||
| `TRAP_DIV_ZERO` | Divide by zero | Division/modulo by zero |
|
||||
| `TRAP_INVALID_FUNC` | Invalid function | Function index not present in function table |
|
||||
| `TRAP_BAD_RET_SLOTS` | Bad return slots | Stack height mismatch at return |
|
||||
|
||||
### 5.3 System
|
||||
|
||||
| Code | Name | Meaning |
|
||||
| ---------------------- | --------------- | --------------------------------------- |
|
||||
| `TRAP_INVALID_SYSCALL` | Invalid syscall | Unknown syscall ID |
|
||||
| `TRAP_STACK_UNDERFLOW` | Stack underflow | Missing arguments for syscall or opcode |
|
||||
|
||||
> This list is **closed for PBS v0** unless explicitly extended.
|
||||
|
||||
---
|
||||
|
||||
## 6. Trap Semantics
|
||||
|
||||
### 6.1 Execution
|
||||
|
||||
When a trap occurs:
|
||||
|
||||
1. The current instruction **does not complete**
|
||||
2. No partial side effects are committed
|
||||
3. Execution stops and returns `TrapInfo` to the host
|
||||
|
||||
### 6.2 Stack & Frames
|
||||
|
||||
* Operand stack is left in a **valid but unspecified** state
|
||||
* Call frames above the trapping frame are not resumed
|
||||
|
||||
### 6.3 Host Policy
|
||||
|
||||
The host decides:
|
||||
|
||||
* whether the trap terminates the whole program
|
||||
* whether execution may be restarted
|
||||
* how the trap is surfaced to the user (error, log, UI, etc.)
|
||||
|
||||
---
|
||||
|
||||
## 7. Verifier Interaction
|
||||
|
||||
The verifier **must prevent** traps that are statically provable, including:
|
||||
|
||||
* stack underflow
|
||||
* invalid control-flow joins
|
||||
* invalid syscall IDs
|
||||
* incorrect return slot counts
|
||||
|
||||
If a verifier rejects a module, **no runtime traps should occur for those causes**.
|
||||
|
||||
---
|
||||
|
||||
## 8. What Is *Not* a Trap
|
||||
|
||||
The following are **VM bugs or tooling errors**, not traps:
|
||||
|
||||
* handler returns wrong number of slots
|
||||
* opcode implementation violates `OpcodeSpec`
|
||||
* verifier and runtime disagree on stack effects
|
||||
|
||||
These must result in **VM panic**, not a trap.
|
||||
|
||||
---
|
||||
|
||||
## 9. Versioning Policy
|
||||
|
||||
* Trap codes are **ABI-stable within a major version** (v0)
|
||||
* New trap codes may only be added in a **new major ABI version** (v1)
|
||||
* Removing or reinterpreting trap codes is forbidden
|
||||
|
||||
---
|
||||
|
||||
## 10. Summary
|
||||
|
||||
Runtime traps are:
|
||||
|
||||
* an explicit part of the Prometeu execution model
|
||||
* deterministic and ABI-stable
|
||||
* reserved for **user-program semantic errors**
|
||||
|
||||
They are **not** debugging tools and **not** VM panics.
|
||||
|
||||
This spec formalizes existing behavior and freezes it for PBS v0.
|
||||
|
||||
---
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,359 +0,0 @@
|
||||
# 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
|
||||
5
scripts/run-local.sh
Executable file
5
scripts/run-local.sh
Executable file
@ -0,0 +1,5 @@
|
||||
#!/bin/bash
|
||||
set -e
|
||||
|
||||
cargo run -p pbxgen-stress
|
||||
cargo run -p prometeu-host-desktop-winit --release -- --run test-cartridges/stress-console
|
||||
Loading…
x
Reference in New Issue
Block a user