Adapted from DLR-FT's Wasm interpreter.
| ID | Title | Statement | Rationale |
|---|---|---|---|
| REQ-1 | Resumable | The interpreter shall be resumable. | Operation with a bounded run-time requires that the interpreter can be halted and later resumed as if it was never halted. |
| REQ-2 | No native/host stack | The interpreter shall not use the native/host stack to implement interpreted function calls. | The interpreted stack lives in a traditional data structure (e.g. Vec<u8>) rather than host function calls, so interpretation can be interrupted between any two virtual instructions and resumed from there. |
| REQ-3 | Baremetal | The interpreter shall be executable on bare-metal environments. | No reliance on any specific functionality from the execution environment, so the interpreter can be embedded in any environment the language can compile for. |
| REQ-4 | No implicit heap | The interpreter shall not rely on a default panicking allocator; any allocator must return a permissive (non-panicking) result for failed allocations. | A stock alloc panics on allocation failure, which is unacceptable on bare environments without an operating system. |
| REQ-5 | Configurable bounded execution | The interpreter shall yield back control flow eventually, within a configurable bound, and support fuel-bounded execution. | A user shall be able to call the interpreter with a bound and expect a result in a finite number of bytecode operations, even for non-terminating bytecode. Fuel is the mechanism: each instruction consumes a fixed amount of fuel and the interpreter yields when fuel is insufficient, resuming later. |
| REQ-6 | Instrumentation | The interpreter shall implement means for instrumentation. | Instrumentation generates evidence for certification, eases debugging, and enables run-time monitoring. |
| REQ-7 | Migrateable | The interpreter state shall be able to halt on one computer and continue execution on another. | Enables load-balancing and redundancy: running applications migrate between computers without disruption. |
| REQ-8 | De-/Serializable | The interpreter state shall be de-/serializable to and from a canonical representation. | A canonical serializable state makes migration and check-point/lock-step execution simple. |
| REQ-9 | No Dependencies | No dependencies but those explicitly allowed by a requirement shall be used. | Dependencies must undergo the full V&V process, which adds enormous work. Exceptions must reference this requirement as parent and pin an exact version (major.minor.patch). |
| REQ-10 | Fixed, cappable memory | The interpreter shall operate on a fixed memory and be able to cap it. | Bounding memory is required for deterministic behavior on constrained targets. |
| REQ-11 | Bounded dynamic allocation | Dynamic allocation shall occur exclusively during module initialization, be limited to a maximum set of fixed-size pages, grow strictly during init, remain constant during execution, and be freed at completion. | Confining allocation to init with a fixed page cap eliminates fragmentation and keeps execution-time memory constant. |
| REQ-12 | Allow libm dependency |
The interpreter may depend on libm 0.2.8, provided it can be built from source. |
no_std targets don't expose all floating-point ops (abs, ceil, floor, trunc, round, sqrt, copysign) without a C libm. |
| REQ-13 | Target Wasm specification | The interpreter shall target Wasm 1.0 Recommendation (MVP + mutable globals), with select post-MVP proposals adopted to support wasm32-unknown-unknown rather than wasm32v1-none. |
Smaller binaries and faster execution for low complexity overhead. |
| REQ-14 | Decoding / validation bounds | Decoding and validation shall be bounded and able to halt, consistent with the execution bound. | Decoding and validation must not run unbounded, especially under streaming. |
| REQ-15 | Streaming / chunked decode | The interpreter shall support providing the .wasm binary in chunks, processing each chunk as it arrives. |
Avoids allocating one contiguous region large enough for the entire binary. Pairs with a 16-bit-aligned IR held in pages that point to each other, boosting execution speed; the raw Wasm binary need not be retained. |
| REQ-16 | Disallow memory.grow |
memory.grow shall be optionally rejected at decoding time. |
Allows restriction to a subset of programs that have determinisic memory characteristics. |
| REQ-17 | Ground memory-measurement tool | A ground tool shall be provided to measure memory usage. | Enables verifying and reporting the interpreter's memory footprint. |