clean up
This commit is contained in:
parent
9ac48379ed
commit
8152269d5b
SSH Key Fingerprint:
SHA256:Z7dgqoglWwoK6j6u4QC87OveEq74WOhFN+gitsxtkf8
@ -1,198 +0,0 @@
|
||||
Mini Spec — Borrow/Mutate Views on a GC Heap (Prometeu)
|
||||
|
||||
This document defines an optional “Rust-flavored” access discipline for heap objects without using RC/HIP. It is compatible with a GC-based heap, first-class functions (closures), and deterministic coroutines.
|
||||
|
||||
Goals
|
||||
|
||||
Preserve the feel of borrow (shared read) and mutate (exclusive write).
|
||||
|
||||
Prevent common aliasing bugs in user code.
|
||||
|
||||
Keep the runtime simple and GC-friendly.
|
||||
|
||||
Avoid restrictions that would block closures/coroutines.
|
||||
|
||||
Non-goals
|
||||
|
||||
Not a full Rust borrow checker.
|
||||
|
||||
Not a memory management mechanism (GC owns lifetimes).
|
||||
|
||||
Not a general concurrency/locking system.
|
||||
|
||||
1. Concepts
|
||||
1.1 Heap handle
|
||||
|
||||
A heap object is referenced by a handle. Handles can be stored, copied, captured, and returned freely (GC-managed).
|
||||
|
||||
1.2 Views
|
||||
|
||||
A view is a temporary capability derived from a handle:
|
||||
|
||||
BorrowView<T>: shared read-only view
|
||||
|
||||
MutView<T>: exclusive mutable view
|
||||
|
||||
Views are stack-only and lexically scoped.
|
||||
|
||||
2. Core Rules (Language Semantics)
|
||||
2.1 Creating views
|
||||
|
||||
Views can be created only by dedicated constructs:
|
||||
|
||||
borrow(h) { ... } produces a BorrowView for the duration of the block
|
||||
|
||||
mutate(h) { ... } produces a MutView for the duration of the block
|
||||
|
||||
2.2 View locality
|
||||
|
||||
Views must never escape their lexical scope:
|
||||
|
||||
A view cannot be:
|
||||
|
||||
stored into heap objects
|
||||
|
||||
captured by closures
|
||||
|
||||
returned from functions
|
||||
|
||||
yielded across coroutine suspension points
|
||||
|
||||
stored into globals
|
||||
|
||||
(Think: “views are ephemeral; handles are persistent.”)
|
||||
|
||||
2.3 Access permissions
|
||||
|
||||
Within a view scope:
|
||||
|
||||
BorrowView permits reads only
|
||||
|
||||
MutView permits reads and writes
|
||||
|
||||
Outside a view scope:
|
||||
|
||||
direct field access is not permitted; you must open a view scope again.
|
||||
|
||||
2.4 Exclusivity
|
||||
|
||||
At any program point, for a given handle h:
|
||||
|
||||
Multiple BorrowView(h) may coexist.
|
||||
|
||||
Exactly one MutView(h) may exist, and it excludes all borrows.
|
||||
|
||||
This is enforced at compile time (required) and optionally at runtime in debug mode (see §5).
|
||||
|
||||
2.5 Re-entrancy
|
||||
|
||||
Within a mutate(h) scope:
|
||||
|
||||
nested borrow(h) is allowed (it is trivially compatible)
|
||||
|
||||
nested mutate(h) is disallowed
|
||||
|
||||
Within a borrow(h) scope:
|
||||
|
||||
nested mutate(h) is disallowed
|
||||
|
||||
3. Interaction with Closures and Coroutines
|
||||
3.1 Closures
|
||||
|
||||
Closures may capture handles freely.
|
||||
|
||||
Closures must not capture views.
|
||||
|
||||
If code inside borrow/mutate creates a closure, it may capture the handle, but not the view.
|
||||
|
||||
3.2 Coroutines
|
||||
|
||||
Coroutines may store handles in their stacks/locals.
|
||||
|
||||
Views must not live across suspension:
|
||||
|
||||
A coroutine cannot yield while a view is active.
|
||||
|
||||
A coroutine cannot sleep while a view is active.
|
||||
|
||||
This rule guarantees that view lifetimes remain local and deterministic.
|
||||
|
||||
4. Compiler Requirements (Static Enforcement)
|
||||
|
||||
The compiler enforces this feature by tracking view lifetimes as lexical regions.
|
||||
|
||||
Minimum checks:
|
||||
|
||||
A view cannot be assigned to a variable with heap lifetime.
|
||||
|
||||
A view cannot appear in a closure capture set.
|
||||
|
||||
A view cannot be returned.
|
||||
|
||||
A view cannot be live at FRAME_SYNC, YIELD, SLEEP, or any safe-point boundary defined by the language.
|
||||
|
||||
Exclusivity rules per handle region (borrow vs mutate overlaps) must hold.
|
||||
|
||||
If a rule is violated: compile error (fatal).
|
||||
|
||||
5. Optional Runtime Checking (Debug Mode)
|
||||
|
||||
Runtime checking is optional and intended for debugging or untrusted bytecode scenarios.
|
||||
|
||||
5.1 Object header borrow-state
|
||||
|
||||
Each heap object may maintain:
|
||||
|
||||
readers: u16
|
||||
|
||||
writer: bool
|
||||
|
||||
Runtime actions:
|
||||
|
||||
entering borrow increments readers if no writer
|
||||
|
||||
leaving borrow decrements readers
|
||||
|
||||
entering mutate requires readers==0 and writer==false, then sets writer=true
|
||||
|
||||
leaving mutate sets writer=false
|
||||
|
||||
Violations trap with a specific diagnostic.
|
||||
|
||||
5.2 Build profiles
|
||||
|
||||
Release builds may omit this entirely (zero overhead).
|
||||
|
||||
Debug builds may enable it.
|
||||
|
||||
6. Lowering to Bytecode (Suggested)
|
||||
|
||||
This feature does not require dedicated opcodes in the minimal design.
|
||||
|
||||
Recommended lowering strategy:
|
||||
|
||||
borrow/mutate are compile-time constructs.
|
||||
|
||||
Field reads/writes lower to existing heap access opcodes (FIELD_GET/FIELD_SET or equivalent), but only permitted while a view is considered “active” by the compiler.
|
||||
|
||||
In debug-runtime-check mode, the compiler may insert explicit enter/exit markers (or syscalls) to enable runtime enforcement.
|
||||
|
||||
7. Rationale
|
||||
|
||||
GC removes the need for RC/HIP, but aliasing mistakes still exist. Views provide a clean and didactic discipline:
|
||||
|
||||
Handles: long-lived, capturable, GC-managed.
|
||||
|
||||
Views: short-lived, local, safe access windows.
|
||||
|
||||
This keeps the VM simple while enabling expressive language features (closures, coroutines) without lifetime headaches.
|
||||
|
||||
8. Summary
|
||||
|
||||
Borrow/Mutate are access disciplines, not memory management.
|
||||
|
||||
Views are stack-only and non-escapable.
|
||||
|
||||
Closures and coroutines freely use handles, but never views.
|
||||
|
||||
Enforcement is compile-time, with optional runtime checks in debug mode.
|
||||
186
files/LOAD.md
186
files/LOAD.md
@ -1,186 +0,0 @@
|
||||
# PR-6 — PBX Declared Syscalls Section (Load-Time Resolution Integration)
|
||||
|
||||
## Briefing
|
||||
|
||||
Chapter 16 requires that cartridges declare required syscalls using canonical identities `(module, name, version)` and that these be resolved at load time before the VM begins execution.
|
||||
|
||||
Until now, resolution has existed only as an API (PR5.3.2). The PBX on-disk format currently does not carry declared syscalls, and the loader cannot enforce load-time resolution deterministically.
|
||||
|
||||
This PR introduces a minimal, production-grade PBX section for **declared syscalls only** and integrates it into the PBX load sequence.
|
||||
|
||||
**Scope note (important):**
|
||||
|
||||
* PBX contains **program + syscall metadata** only.
|
||||
* Assets (`asset_table`, `preload`, etc.) are explicitly **out of scope** for this PR and will be handled later via `asset.pa`.
|
||||
|
||||
After this PR:
|
||||
|
||||
* `program.pbx` contains a `SYSC` (declared syscalls) section.
|
||||
* The PBX loader parses `SYSC` and resolves identities at load time.
|
||||
* Load fails deterministically if resolution fails.
|
||||
* The VM continues to execute `SYSCALL <id>` only.
|
||||
|
||||
No backward compatibility. No fallback to external manifests in production.
|
||||
|
||||
---
|
||||
|
||||
## Target
|
||||
|
||||
1. Define a minimal PBX section for declared syscalls.
|
||||
2. Extend the PBX parser/loader to read this section.
|
||||
3. Integrate `resolve_program_syscalls()` into PBX load.
|
||||
4. Enforce load-time failure on unknown or unauthorized syscalls.
|
||||
5. Keep VM runtime strictly numeric.
|
||||
|
||||
---
|
||||
|
||||
## PBX Section Format (Authoritative for This PR)
|
||||
|
||||
Add a new PBX chunk:
|
||||
|
||||
* Chunk ID: `SYSC`
|
||||
|
||||
Binary layout:
|
||||
|
||||
```
|
||||
u32 count
|
||||
repeat count times:
|
||||
u16 module_len
|
||||
[module_len bytes UTF-8]
|
||||
u16 name_len
|
||||
[name_len bytes UTF-8]
|
||||
u16 version
|
||||
```
|
||||
|
||||
Rules:
|
||||
|
||||
* UTF-8 strings only.
|
||||
* No string table in this PR (keep it minimal).
|
||||
* This section is REQUIRED for PBX v0 after this PR.
|
||||
* If absent → load error.
|
||||
* Duplicate `(module,name,version)` entries → load error.
|
||||
|
||||
**Out of scope:** Any asset-related metadata. Do not add `ASSET_TABLE`, `PRELOAD`, or anything similar to PBX in this PR.
|
||||
|
||||
---
|
||||
|
||||
## Load Sequence (After PR-6)
|
||||
|
||||
1. Parse PBX header and TOC.
|
||||
2. Parse `SYSC` section into `Vec<SyscallIdentity>`.
|
||||
3. Call:
|
||||
|
||||
```rust
|
||||
resolve_program_syscalls(&declared, vm.capabilities)
|
||||
```
|
||||
4. If resolution fails → abort load deterministically.
|
||||
5. Store resolved syscalls inside VM (or a `LoadedProgram` struct).
|
||||
6. Start VM execution.
|
||||
|
||||
No runtime name resolution allowed.
|
||||
|
||||
---
|
||||
|
||||
## Work Items
|
||||
|
||||
### 1) PBX Parser / Loader Extension
|
||||
|
||||
* Add support for `SYSC` chunk in the PBX parser/loader.
|
||||
* Return `declared_syscalls: Vec<SyscallIdentity>` as part of `ProgramImage` (or equivalent).
|
||||
* If `SYSC` is missing → return load error.
|
||||
|
||||
### 2) Load-Time Resolver Integration
|
||||
|
||||
* In the PBX load path:
|
||||
|
||||
* Parse declared syscalls.
|
||||
* Resolve using `prometeu_hal::syscalls::resolve_program_syscalls`.
|
||||
* Enforce capability checks at load time.
|
||||
* If resolution fails → load fails (no runtime fallback).
|
||||
|
||||
* Do NOT modify VM execution core beyond storing the resolved mapping.
|
||||
|
||||
### 3) VM State Storage
|
||||
|
||||
* Add or finalize storage for resolved syscalls (if not already present).
|
||||
* VM must NOT use canonical strings at runtime.
|
||||
* VM runtime continues to execute only numeric IDs.
|
||||
|
||||
### 4) Error Handling
|
||||
|
||||
PBX load must fail deterministically if:
|
||||
|
||||
* Unknown `(module,name,version)`.
|
||||
* Capability mismatch.
|
||||
* Duplicate identities in `SYSC`.
|
||||
* `SYSC` chunk is missing.
|
||||
* Malformed `SYSC` payload (lengths/UTF-8).
|
||||
|
||||
Errors must be explicit and deterministic.
|
||||
|
||||
---
|
||||
|
||||
## Acceptance Checklist
|
||||
|
||||
* [ ] PBX format supports `SYSC` chunk.
|
||||
* [ ] Loader parses declared syscalls from PBX.
|
||||
* [ ] Resolver runs during PBX load (before VM execution).
|
||||
* [ ] Load fails on unknown syscall.
|
||||
* [ ] Load fails on capability violation.
|
||||
* [ ] Load fails when `SYSC` chunk is missing.
|
||||
* [ ] No runtime name resolution exists.
|
||||
* [ ] `cargo test` passes.
|
||||
|
||||
---
|
||||
|
||||
## Tests
|
||||
|
||||
Add tests covering:
|
||||
|
||||
1. Valid PBX with one syscall identity → loads successfully.
|
||||
2. PBX with unknown syscall identity → load error.
|
||||
3. PBX with capability violation → load error.
|
||||
4. PBX without `SYSC` section → load error.
|
||||
5. PBX with duplicate identity entries → load error.
|
||||
6. PBX with malformed `SYSC` payload (bad lengths/invalid UTF-8) → load error.
|
||||
|
||||
Tests must construct minimal synthetic PBX images in-memory.
|
||||
|
||||
Do NOT rely on external files.
|
||||
|
||||
---
|
||||
|
||||
## Junie Instructions
|
||||
|
||||
You MAY:
|
||||
|
||||
* Extend PBX parser/loader to support `SYSC`.
|
||||
* Integrate the resolver into the PBX load path.
|
||||
* Add deterministic tests for load-time resolution.
|
||||
|
||||
You MUST NOT:
|
||||
|
||||
* Add backward compatibility paths.
|
||||
* Add fallback to JSON manifests.
|
||||
* Add any asset-table or preload metadata to PBX.
|
||||
* Change VM runtime dispatch logic.
|
||||
* Modify syscall numeric IDs.
|
||||
|
||||
If PBX container format details (header/TOC/chunk reading) are unclear:
|
||||
|
||||
* STOP.
|
||||
* Ask for clarification before inventing new unrelated chunk structures.
|
||||
|
||||
No assumptions beyond the `SYSC` layout defined above.
|
||||
|
||||
---
|
||||
|
||||
## Definition of Done
|
||||
|
||||
After this PR:
|
||||
|
||||
* Syscall resolution is fully load-time for PBX.
|
||||
* PBX is authoritative for declared syscalls.
|
||||
* VM executes only numeric syscalls.
|
||||
* No legacy or dev fallback exists in the production load path.
|
||||
* No asset responsibilities are added to PBX.
|
||||
@ -1,44 +0,0 @@
|
||||
Layered Test Suite Architecture (PR‑8.3)
|
||||
|
||||
Overview
|
||||
|
||||
- Tests are organized by runtime layer to isolate failures and clarify ownership of behavior.
|
||||
- Location: `crates/dev/prometeu-layer-tests/tests/`
|
||||
|
||||
Layers and representative tests
|
||||
|
||||
1. Bytecode encode/decode
|
||||
- `bytecode_encode_decode.rs` — round‑trip decoding for edge immediates and structure.
|
||||
2. Verifier
|
||||
- `verifier_closure_reject.rs` — rejects `CALL_CLOSURE` when TOS is not a closure.
|
||||
- Rule: verifier tests never run the VM.
|
||||
3. VM execution
|
||||
- `vm_exec_valid.rs` — executes a tiny valid program; assumes verified input.
|
||||
- Rule: VM tests do not depend on the verifier; they prepare ROM directly.
|
||||
4. GC behavior
|
||||
- `gc_collect_unreachable.rs` — unrooted closure is reclaimed; rooted one survives.
|
||||
5. Scheduler behavior
|
||||
- `scheduler_determinism.rs` — deterministic FIFO ordering for same‑tick wakeups.
|
||||
|
||||
Running the layered suite
|
||||
|
||||
- Run just the layered tests: `cargo test -p prometeu-layer-tests`
|
||||
- Run the entire workspace: `cargo test`
|
||||
|
||||
Host debugger socket tests
|
||||
|
||||
- The host debugger integration tests in `crates/host/prometeu-host-desktop-winit/src/runner.rs` open localhost TCP ports and are marked `#[ignore]` in the default test flow.
|
||||
- This keeps `cargo test --workspace --all-targets --all-features --no-fail-fast` green in restricted environments that forbid `TcpListener::bind`.
|
||||
- Run the socket-dependent suite explicitly with `make test-debugger-socket` or `cargo test -p prometeu-host-desktop-winit --lib -- --ignored`.
|
||||
- These tests must still run in at least one official environment that permits localhost bind/connect.
|
||||
|
||||
Separation of concerns
|
||||
|
||||
- No cross‑layer assumptions in these tests.
|
||||
- Verifier tests: no `VirtualMachine` execution.
|
||||
- VM tests: assume pre‑verified bytecode; interact via public VM APIs only.
|
||||
- GC and Scheduler tests: exercise their public APIs directly, without booting the VM.
|
||||
|
||||
DRY helpers
|
||||
|
||||
- Shared utilities should live in `crates/dev/prometeu-test-support` when needed. The current minimal suite avoids duplication by using tiny local helpers.
|
||||
Loading…
x
Reference in New Issue
Block a user