12 KiB
PR-2 - PBX SYSC and HOSTCALL Loader Patching
Goal
Teach the runtime to load canonical host bindings from PBX, resolve them at load time, validate ABI and capabilities, and rewrite pre-load host calls into final numeric syscalls.
This PR assumes PR-1 is already available, so cartridge capabilities are exposed to the loader as internal CapFlags.
Why
Prometeu's hardware contract is:
- source- and SDK-level host APIs map to canonical identities
(module, name, version) - load-time resolution maps those identities to numeric syscall ids
- runtime execution is numeric-only via
SYSCALL <id>
The runtime already has the important building blocks:
- canonical syscall registry
- load-time
resolve_program_syscalls - verifier support for numeric
SYSCALL <id> - VM dispatch by numeric id
What is missing is the PBX and loader wiring.
Scope
In scope:
- add a mandatory PBX
SYSCsection - extend each
SYSCentry with ABI shape - add pre-load opcode
HOSTCALL <sysc_index> - parse
SYSCat load time - resolve
SYSCagainst the host syscall registry - validate declared ABI against authoritative host metadata
- validate capabilities using cartridge-granted
CapFlags - reject unused
SYSCentries - reject out-of-bounds
HOSTCALLindices - patch all
HOSTCALL <sysc_index>toSYSCALL <id> - ensure verifier runs only on the patched image
Out of scope:
- compiler emission
- stdlib SDK pack format
- final external tooling for PBX generation
- platform policy beyond current manifest-derived granted capabilities
Architectural Contract
PBX SYSC
SYSC is a unique, deduplicated, program-wide table of declared host bindings.
Each entry carries:
modulenameversionarg_slotsret_slots
SYSC is mandatory for every valid PBX.
If the program requires no host bindings, SYSC is present with count = 0.
Pre-load callsites
The compiler-side artifact form is:
HOSTCALL <u32 sysc_index>
Rules:
sysc_indexis zero-based into theSYSCtable- code must not contain final
SYSCALL <id>for unresolved host-backed SDK calls - the final executable image given to the VM must contain no
HOSTCALL
Load-time responsibilities
The loader must:
- parse
SYSC - resolve each entry to
syscall_id - validate
arg_slotsandret_slots - validate capabilities
- scan code for
HOSTCALL - mark used
SYSCindices - reject out-of-bounds indices
- reject unused
SYSCentries - rewrite
HOSTCALL <index>intoSYSCALL <id> - ensure no
HOSTCALLremains - only then hand the image to the verifier
PBX Format Changes
prometeu-bytecode
Add a new section kind:
SYSC
Recommended temporary 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
u16 arg_slots
u16 ret_slots
Rules:
- strings are UTF-8
- duplicate canonical identities are invalid
- malformed lengths are invalid
- missing
SYSCis invalid
Bytecode model changes
Extend BytecodeModule with a syscall declaration vector.
Suggested shape:
pub struct SyscallDecl {
pub module: String,
pub name: String,
pub version: u16,
pub arg_slots: u16,
pub ret_slots: u16,
}
Then:
pub syscalls: Vec<SyscallDecl>
Serialization/deserialization must include section kind for SYSC.
Opcode Changes
Add HOSTCALL
Add a new opcode:
HOSTCALL
Immediate:
u32 sysc_index
Recommended behavior:
- valid only in pre-load artifact form
- not allowed to reach final verifier/VM execution path
Required code updates:
- opcode enum
- decoder
- opcode spec
- assembler
- disassembler
Verifier recommendation:
- the verifier does not need to support
HOSTCALL - it should continue to run after loader patching only
Loader Integration
Resolution
Use the existing canonical resolver in prometeu-hal::syscalls.
For each SYSC entry:
- resolve
(module, name, version) - obtain
SyscallResolved - compare
arg_slots - compare
ret_slots - compare required capability against granted cartridge flags
If any check fails, load fails deterministically.
Capability source
Capabilities come from the already-loaded cartridge manifest via PR-1.
This PR must not invent authority from PBX contents.
Code patching
Recommended algorithm:
- parse code buffer
- whenever
HOSTCALL <index>is found: - validate
index < syscalls.len() - mark that
SYSC[index]is used - rewrite opcode/immediate in place or rebuild the code buffer
- emit final
SYSCALL <resolved_id>
After scan:
- every
SYSCentry must be marked used - no
HOSTCALLmay remain
Either patching strategy is acceptable:
- mutate byte buffer in place
- rebuild a fresh patched buffer
The final ProgramImage must contain only numeric SYSCALL <id>.
Verifier Contract
No verifier redesign is required.
The intended contract is:
- loader validates interface compatibility
- verifier validates final numeric program structure
This means:
- loader checks
SYSC-declared ABI against host metadata - verifier checks stack effects of final
SYSCALL <id>using existing runtime metadata
This is intentional and not considered harmful duplication.
Proposed Code Areas
prometeu-bytecode
Likely files:
src/model.rssrc/opcode.rssrc/opcode_spec.rssrc/decoder.rssrc/assembler.rssrc/disassembler.rssrc/lib.rs
prometeu-hal
Likely files:
src/cartridge_loader.rs- possibly helper types or resolver glue near syscall loading logic
prometeu-vm
Likely files:
- load path in
src/virtual_machine.rs
Required behavior:
- patch before
Verifier::verify(...)
Implementation Plan
Implementation should be staged so each phase leaves the workspace in a coherent state and keeps the verifier/VM contract intact.
Commit Checklist
prometeu-bytecode: add SyscallDecl model and mandatory SYSC sectionprometeu-bytecode: add SYSC parser validation and load errorsprometeu-bytecode: add phase-1 coverage for empty/valid/invalid SYSCprometeu-bytecode: wire downstream constructors to new BytecodeModule.syscalls fieldprometeu-bytecode: clean up naming/docs after phase-1 passes
Phase 1 - Extend PBX module format
Target crates:
crates/console/prometeu-bytecode
Steps:
- add
SyscallDecltosrc/model.rsand extendBytecodeModulewithsyscalls: Vec<SyscallDecl> - reserve a new section kind for
SYSCin module serialization/deserialization - enforce the mandatory-section rule: valid PBS images always carry
SYSC, includingcount = 0 - reject malformed payloads, invalid UTF-8, and duplicate canonical identities during load
- update
src/lib.rsexports if needed so the VM and HAL can consume the new declarations
Checkpoint:
BytecodeLoader::load(...)returnsBytecodeModulewith canonical syscall declarations preserved from PBX
Phase 2 - Add pre-load opcode support
Target crates:
crates/console/prometeu-bytecode
Steps:
- add
HOSTCALLtosrc/opcode.rswith au32immediate - extend
src/opcode_spec.rsandsrc/decoder.rsso the loader can scan and decodeHOSTCALL - update
src/assembler.rsandsrc/disassembler.rsso tests and fixtures can produce/read pre-load artifacts - keep the runtime contract explicit:
HOSTCALLis representable in bytecode artifacts but must not survive loader patching
Checkpoint:
- bytecode tooling round-trips
HOSTCALL <index>correctly, while runtime execution still depends on patchedSYSCALL <id>
Phase 3 - Bridge PBX declarations to host metadata
Target crates:
crates/console/prometeu-hal
Steps:
- add a resolver path that accepts program-owned syscall declarations instead of only
&'static stridentities - resolve each
(module, name, version)againstsrc/syscalls.rs - validate
arg_slotsandret_slotsagainst authoritativeSyscallMeta - validate required capabilities against cartridge-derived
CapFlags - return deterministic, load-facing errors for unknown syscalls, ABI mismatches, and missing capabilities
Design note:
- this phase likely needs a small owned-string adapter or a new helper alongside
resolve_program_syscalls(...), because PBX strings are runtime data, not&'static str
Checkpoint:
- given only
BytecodeModule.syscallsplus grantedCapFlags, the loader can produce a resolved tablesysc_index -> syscall_id
Phase 4 - Patch before verification
Target crates:
crates/console/prometeu-vm
Steps:
- add a load-time patching helper near
src/virtual_machine.rsor a small dedicated module - run that helper immediately after
BytecodeLoader::load(...)and beforeVerifier::verify(...) - scan
module.code, decode every instruction, and rewriteHOSTCALL <index>intoSYSCALL <resolved_id> - reject out-of-bounds
HOSTCALLindices during the scan - track
SYSCusage and reject declarations that are never referenced - assert that no
HOSTCALLremains before handing code to the verifier - only then call
Verifier::verify(...), computemax_stack_slots, and buildProgramImage::from(module)
Why the sequencing matters:
- the current load path in
crates/console/prometeu-vm/src/virtual_machine.rsverifies the raw module immediately afterBytecodeLoader::load(...) ProgramImagecurrently stores only the final ROM/functions/constants and does not preserve a syscall declaration table, so patching must happen while the code is still aBytecodeModule
Checkpoint:
- the verifier sees only numeric
SYSCALL <id>instructions, preserving the existing verifier and VM execution model
Phase 5 - Tests and failure matrix
Target crates:
crates/console/prometeu-bytecodecrates/console/prometeu-halcrates/console/prometeu-vm
Steps:
- add serialization/deserialization tests for missing, empty, valid, malformed, and duplicate
SYSC - add opcode tests for
HOSTCALLdecoding and assembler/disassembler coverage - add resolver tests for unknown identity, ABI mismatch, and capability mismatch
- add VM load-path tests proving patch-before-verify behavior
- add an assertion that final executable images contain only numeric
SYSCALL
Suggested PR slicing:
- bytecode format + tests
HOSTCALLopcode plumbing- HAL resolution/ABI validation
- VM loader patching
- integration and regression tests
Deterministic Load Errors
Load must fail for at least:
- missing
SYSC - malformed
SYSC - invalid UTF-8
- duplicate syscall identities
- unknown syscall identity
- ABI mismatch between
SYSCand host metadata - missing capability
HOSTCALLwith out-of-boundssysc_index- declared
SYSCentry unused by allHOSTCALLs HOSTCALLstill present after patch
Acceptance Criteria
- PBX parser supports mandatory
SYSC BytecodeModulecarries syscall declarations- runtime understands
HOSTCALL - loader resolves
SYSCentries before verification - loader validates
arg_slotsandret_slots - loader validates capabilities against cartridge flags
- loader rewrites
HOSTCALLtoSYSCALL - verifier runs only on patched code
- final VM execution path remains numeric-only
Tests
Add tests covering:
- valid PBX with empty
SYSCand noHOSTCALL - valid PBX with one syscall and one
HOSTCALL - unknown syscall identity
- capability mismatch
- ABI mismatch
- missing
SYSC - duplicate
SYSCentries - malformed
SYSCpayload HOSTCALLindex out of bounds- unused
SYSCentry - patched image contains only
SYSCALL
Prefer synthetic in-memory PBX images in tests.
Definition of Done
After this PR:
- PBX declares canonical host bindings in
SYSC - pre-load code references those bindings with
HOSTCALL - the loader resolves and validates them during load
- the loader patches executable code to
SYSCALL <id> - the verifier and VM continue to operate on numeric syscalls only