603 lines
12 KiB
Markdown
603 lines
12 KiB
Markdown
# PR-4.2 — Basic Stack Safety Verification (Underflow/Overflow)
|
|
|
|
### Briefing
|
|
|
|
The verifier must ensure the stack never underflows or exceeds defined limits during execution.
|
|
|
|
### Target
|
|
|
|
* Implement stack safety checks across the control-flow graph.
|
|
|
|
### Work items
|
|
|
|
* Simulate stack depth across instructions.
|
|
* Detect:
|
|
|
|
* Stack underflow.
|
|
* Stack overflow beyond declared limits.
|
|
* Emit appropriate verifier errors.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Underflow cases are rejected.
|
|
* [ ] Overflow cases are rejected.
|
|
* [ ] Valid programs pass.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Program with underflow → verifier error.
|
|
* Program exceeding stack limit → verifier error.
|
|
* Valid program → passes.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Add stack depth simulation.
|
|
* Introduce verifier error types.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change runtime stack implementation.
|
|
* Introduce dynamic stack resizing.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before choosing stack limit rules.
|
|
|
|
---
|
|
|
|
# PR-4.3 — Control Flow and Jump Target Verification
|
|
|
|
### Briefing
|
|
|
|
The verifier must ensure all control flow transfers are valid and do not jump into the middle of instructions or outside function boundaries.
|
|
|
|
### Target
|
|
|
|
* Validate all jump targets.
|
|
* Reject invalid or unsafe control flow.
|
|
|
|
### Work items
|
|
|
|
* Use canonical layout utilities to identify instruction boundaries.
|
|
* Verify:
|
|
|
|
* Jump targets land on valid instruction boundaries.
|
|
* Targets are within the function range.
|
|
* Reject invalid targets with a verifier error.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Invalid jump targets are rejected.
|
|
* [ ] Valid programs pass verification.
|
|
* [ ] No reliance on runtime traps for these cases.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Jump to middle of instruction → verifier error.
|
|
* Jump outside function → verifier error.
|
|
* Valid jump → passes.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Reuse layout utilities for boundary checks.
|
|
* Add verifier error cases.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Modify instruction encoding.
|
|
* Introduce new trap codes.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before defining jump rules.
|
|
|
|
---
|
|
|
|
# PR-4.4 — Function Boundary and Terminator Verification
|
|
|
|
### Briefing
|
|
|
|
Functions must follow canonical entry and exit rules. The verifier must enforce valid terminators and boundaries.
|
|
|
|
### Target
|
|
|
|
* Ensure functions start and end correctly.
|
|
* Ensure terminator instructions are valid.
|
|
|
|
### Work items
|
|
|
|
* Verify function entry points are valid instruction boundaries.
|
|
* Verify function exit instructions:
|
|
|
|
* Proper `RET` usage.
|
|
* Proper `FRAME_SYNC` placement (as per spec).
|
|
* Reject functions without valid termination.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] All functions have valid entry and exit.
|
|
* [ ] Invalid termination is rejected.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Function without terminator → verifier error.
|
|
* Properly terminated function → passes.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Add boundary validation logic.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Redefine function semantics.
|
|
* Change terminator opcode behavior.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before enforcing termination rules.
|
|
|
|
---
|
|
|
|
# PR-4.5 — Multi-Return (`ret_slots`) Verification
|
|
|
|
### Briefing
|
|
|
|
The new ABI supports multi-return via `ret_slots`. The verifier must ensure the stack shape matches the declared return slot count.
|
|
|
|
### Target
|
|
|
|
* Validate return slot counts at call and return sites.
|
|
|
|
### Work items
|
|
|
|
* For each function:
|
|
|
|
* Read declared `ret_slots`.
|
|
* At `RET`:
|
|
|
|
* Ensure stack contains exactly the required number of slots.
|
|
* At call sites:
|
|
|
|
* Ensure caller expects correct number of return slots.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Mismatched return slot counts are rejected.
|
|
* [ ] Correct programs pass.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Too few return slots → verifier error.
|
|
* Too many return slots → verifier error.
|
|
* Correct return slots → passes.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Use function metadata to validate returns.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change calling convention semantics.
|
|
* Modify function metadata layout.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before implementing slot rules.
|
|
|
|
---
|
|
|
|
# PR-4.6 — Verifier Error Model Consolidation
|
|
|
|
### Briefing
|
|
|
|
Verifier errors must be deterministic, structured, and clearly separated from runtime traps.
|
|
|
|
### Target
|
|
|
|
* Introduce a coherent verifier error model.
|
|
|
|
### Work items
|
|
|
|
* Define a `VerifierError` enum covering:
|
|
|
|
* Stack underflow.
|
|
* Stack overflow.
|
|
* Invalid jump target.
|
|
* Invalid function boundary.
|
|
* Return slot mismatch.
|
|
* Ensure verifier returns structured errors.
|
|
* Update tests to expect structured errors.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Verifier errors are structured and deterministic.
|
|
* [ ] No reliance on runtime traps for verifier failures.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Update existing tests to assert specific verifier errors.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Introduce a new verifier error enum.
|
|
* Refactor error returns.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Map verifier errors to runtime traps.
|
|
* Change runtime trap behavior.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before merging or renaming error categories.
|
|
|
|
---
|
|
|
|
# PR-4.7 — Verifier Golden Test Suite
|
|
|
|
### Briefing
|
|
|
|
We need a stable suite of valid and invalid bytecode samples to ensure verifier correctness over time.
|
|
|
|
### Target
|
|
|
|
* Introduce golden tests for the verifier.
|
|
|
|
### Work items
|
|
|
|
* Add a set of small bytecode samples:
|
|
|
|
* Valid programs.
|
|
* Invalid programs for each verifier error.
|
|
* Implement golden tests asserting:
|
|
|
|
* Successful verification.
|
|
* Specific error kinds for invalid programs.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Golden tests exist for all verifier error categories.
|
|
* [ ] Tests are deterministic.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* New golden tests only.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Add deterministic golden tests.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Modify verifier logic to fit tests without understanding the cause.
|
|
* Introduce random or timing-based tests.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before changing test expectations.
|
|
|
|
---
|
|
|
|
# PR-5.1 — Define Canonical Syscall Metadata Table
|
|
|
|
### Briefing
|
|
|
|
Syscalls must follow a unified, function-like ABI based on slot counts and capabilities. This PR introduces the canonical metadata table describing every syscall.
|
|
|
|
### Target
|
|
|
|
* Define a single authoritative metadata structure for syscalls.
|
|
* Ensure all syscalls are described in terms of slot-based ABI.
|
|
|
|
### Work items
|
|
|
|
* Introduce a `SyscallMeta` struct containing:
|
|
|
|
* Syscall identifier.
|
|
* `arg_slots`.
|
|
* `ret_slots`.
|
|
* Capability flags.
|
|
* Determinism flags (if defined in spec).
|
|
* Create a canonical syscall table/registry.
|
|
* Ensure all existing syscalls are registered in this table.
|
|
* Document the structure in code comments (English).
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] All syscalls have a `SyscallMeta` entry.
|
|
* [ ] Metadata includes arg and return slot counts.
|
|
* [ ] No syscall is invoked without metadata.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add a test ensuring all registered syscalls have metadata.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Introduce a syscall metadata struct.
|
|
* Add a central registry for syscalls.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change existing syscall semantics.
|
|
* Add new syscalls.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before defining metadata fields.
|
|
|
|
---
|
|
|
|
# PR-5.2 — Implement Slot-Based Syscall Calling Convention
|
|
|
|
### Briefing
|
|
|
|
Syscalls must behave like functions using the stack-based slot ABI. This PR implements the unified calling convention.
|
|
|
|
### Target
|
|
|
|
* Ensure syscalls read arguments from the stack.
|
|
* Ensure syscalls push return values based on `ret_slots`.
|
|
|
|
### Work items
|
|
|
|
* Modify the VM syscall dispatch logic to:
|
|
|
|
* Look up `SyscallMeta`.
|
|
* Pop `arg_slots` from the stack.
|
|
* Invoke the syscall.
|
|
* Push `ret_slots` results.
|
|
* Remove any legacy argument handling paths.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] All syscalls use slot-based calling convention.
|
|
* [ ] Argument and return slot counts are enforced.
|
|
* [ ] No legacy calling paths remain.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Syscall with correct arg/ret slots → passes.
|
|
* Syscall with insufficient args → trap or verifier failure.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Refactor syscall dispatch code.
|
|
* Use metadata to enforce slot counts.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change the stack model.
|
|
* Add compatibility layers.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before modifying dispatch semantics.
|
|
|
|
---
|
|
|
|
# PR-5.3 — Enforce Capability Checks in Syscall Dispatch
|
|
|
|
### Briefing
|
|
|
|
Syscalls must be capability-gated. The runtime must verify that the current program has permission to invoke each syscall.
|
|
|
|
### Target
|
|
|
|
* Enforce capability checks before syscall execution.
|
|
|
|
### Work items
|
|
|
|
* Extend `SyscallMeta` with capability requirements.
|
|
* Add capability data to the VM or execution context.
|
|
* In syscall dispatch:
|
|
|
|
* Check capabilities.
|
|
* If missing, trigger `TRAP_INVALID_SYSCALL` or equivalent.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Capability checks occur before syscall execution.
|
|
* [ ] Missing capability leads to deterministic trap.
|
|
* [ ] Valid capabilities allow execution.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Syscall without capability → trap.
|
|
* Syscall with capability → success.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Add capability checks in dispatch.
|
|
* Extend metadata with capability fields.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change trap semantics.
|
|
* Introduce dynamic or nondeterministic permission systems.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before defining capability behavior.
|
|
|
|
---
|
|
|
|
# PR-5.4 — Verifier Integration for Syscall Slot Rules
|
|
|
|
### Briefing
|
|
|
|
The verifier must ensure that syscall calls respect argument and return slot counts before runtime.
|
|
|
|
### Target
|
|
|
|
* Extend verifier to validate syscall usage.
|
|
|
|
### Work items
|
|
|
|
* At syscall call sites:
|
|
|
|
* Look up `SyscallMeta`.
|
|
* Ensure enough argument slots are available.
|
|
* Ensure stack shape after call matches `ret_slots`.
|
|
* Emit verifier errors for mismatches.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Verifier rejects incorrect syscall slot usage.
|
|
* [ ] Correct programs pass.
|
|
* [ ] Runtime traps are not required for verifier-detectable cases.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Add tests:
|
|
|
|
* Too few args for syscall → verifier error.
|
|
* Correct args/returns → passes.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Extend verifier with syscall checks.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Change runtime trap logic.
|
|
* Add new trap categories.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before enforcing slot rules.
|
|
|
|
---
|
|
|
|
# PR-5.5 — Remove Legacy Syscall Entry Paths
|
|
|
|
### Briefing
|
|
|
|
Any old or experimental syscall entry paths must be removed so that the slot-based ABI is the only supported mechanism.
|
|
|
|
### Target
|
|
|
|
* Ensure only the new unified syscall dispatch path exists.
|
|
|
|
### Work items
|
|
|
|
* Search for legacy or alternate syscall invocation logic.
|
|
* Remove or refactor them to use the canonical dispatch.
|
|
* Update modules and exports accordingly.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Only one syscall dispatch path remains.
|
|
* [ ] No legacy syscall logic is present.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* Existing tests only.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Remove legacy syscall code paths.
|
|
* Refactor callers to use the unified dispatch.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Introduce new syscall semantics.
|
|
* Keep compatibility shims.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before deleting anything that looks externally visible.
|
|
|
|
---
|
|
|
|
# PR-5.6 — Syscall Multi-Return Tests
|
|
|
|
### Briefing
|
|
|
|
We must ensure multi-return syscalls behave correctly with the slot-based ABI.
|
|
|
|
### Target
|
|
|
|
* Add deterministic tests covering multi-return behavior.
|
|
|
|
### Work items
|
|
|
|
* Create or adapt at least one syscall with `ret_slots > 1`.
|
|
* Add tests:
|
|
|
|
* Verify correct stack results after syscall.
|
|
* Verify incorrect caller expectations fail verification.
|
|
|
|
### Acceptance checklist
|
|
|
|
* [ ] Multi-return syscalls behave correctly.
|
|
* [ ] Verifier catches mismatches.
|
|
* [ ] `cargo test` passes.
|
|
|
|
### Tests
|
|
|
|
* New multi-return syscall tests.
|
|
|
|
### Junie instructions
|
|
|
|
**You MAY:**
|
|
|
|
* Add deterministic tests.
|
|
* Use existing syscalls or create a simple test-only syscall.
|
|
|
|
**You MUST NOT:**
|
|
|
|
* Modify syscall semantics to satisfy tests.
|
|
* Add nondeterministic behavior.
|
|
|
|
**If unclear:**
|
|
|
|
* Ask before introducing new test syscalls.
|
|
|
|
|