Known Limitations

Reference version: 1.0
Implementation snapshot: SekuraJS source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236.

This page lists user-relevant limitations confirmed in the source and tests at the snapshot above. It is not a promise that every unlisted construct or workflow is supported. A source construct that parses or elaborates may still be unsupported by code generation or proof lowering.

Language and compiler

  • sekura-js targets Memora8/MR8. It does not compile to another CPU target, execute the generated program, or provide the MR8 simulator.
  • The language frontend accepts more forms than every type-checking and code-generation path can lower. Some conversion and type rules are incomplete or target-specific; successful parsing alone does not guarantee successful compilation. The language reference marks such areas where identified.
  • Ordinary integer expression results in the MR8 backend use 32-bit values. Do not assume portable ABI, pointer, or mixed-signedness behavior beyond the documented MR8 implementation.
  • Typed array addressing uses element layout, but the compiler does not provide a source-language guarantee of runtime bounds checking.
  • Code generation is MR8-specific; layout and low-level operators are not portable cross-target guarantees.
  • Compilation writes artifacts but does not execute them. A separate MR8 runtime or simulator is needed to run the resulting SOBJ.

SJV model and SJS/SOBJ verification

  • verify-model checks the SJV model and its consistency with the selected source. It does not prove that a compiled SOBJ implements the model. Use verify with the SJV and SOBJ for implementation verification.
  • The SJS/SOBJ verifier’s SMT translator supports a narrower expression subset than the SJV parser. Current supported forms include integer literals, bound simple names, unary minus, addition/subtraction, equality/inequality, ordered comparisons, conjunction, disjunction, and implication. Other parsed expressions can produce an unsupported result.
  • The current MR8 mapping is limited: more than six register parameters are unsupported; modeled global values currently require scalar u32; parameter and return types outside the encoded subset require typed SMT encoding that is not implemented.
  • Unbounded control-flow cycles are not proven without a proven loop bound. Dynamic MMU behavior requires transition contracts; the verifier reports unsupported when those are unavailable.
  • The checked-in verification_identity SJS/SOBJ fixture currently reports FUNCTIONAL UNSUPPORTED for implementation verification because the return target cannot be proven. A successful parse or verify-model result for this fixture is not an implementation proof.
  • For an SJV selecting SystemVerilog, verify-model parses and elaborates but its RTL-to-SMT translation is not implemented. Use the separate SystemVerilog verify path for constructs in that proof subset.

SystemVerilog verification

The SystemVerilog frontend and proof backend implement a defined subset, not a full language implementation, simulator, or synthesis tool.

  • Proof uses a two-state bit-vector model. Four-state X/Z behavior and net-resolution semantics are not modeled.
  • The proof backend accepts only constructs it can lower. Dynamic/runtime-sized data structures, event scheduling, unsupported procedural forms, multiple clock domains, derived clocks, incomplete combinational assignments, and unsupported operators or system functions are outside the proof profile.
  • Fixed proof values are width-limited; the current RTL lowering rejects zero-width and values wider than 1024 bits. Some literal and selection paths have narrower limits. Fixed unpacked arrays used as state are limited to 65,536 elements total.
  • A frontend parse or successful elaboration is not evidence that all behavior was included in the proof. A supported contract and complete proof result are required.
  • SJV proof dependencies are supported only with a SystemVerilog parent. The SJS/SOBJ make-sjv path rejects proof dependencies.

See the SystemVerilog subset reference for construct-level rules and test coverage.

SJP and SOBJ artifacts

  • The current SOBJ loader accepts MR8 object format version 0x00010000; other versions are rejected.
  • Current SJP generation writes format version 2. verify-sjp requires a signed package and an explicitly supplied public key. Legacy line-oriented SJP v1 has no stored SMT payload for replay and is reported as not replayable.
  • make-sjv can successfully write an SJP that records a failed, unsupported, or inconclusive proof result. Package creation is not itself proof success; inspect the recorded result and run verify-sjp on the signed artifact.
  • verify-sjp replays the SMT queries stored in the package. It does not regenerate those queries from the original SJS, SJV, SOBJ, or SystemVerilog inputs, even though their hashes may be recorded. Replay therefore does not establish that the saved formulas were correctly derived from a particular source tree.
  • SJP dependency replay validates recorded package relationships and recursively replays child packages, but it does not re-elaborate child RTL or independently recompute recorded port bindings.

See the SJP format reference, SJP signatures, and compatibility and versioning for format and version details.

Solver and release boundaries

  • Z3 is required for proof commands and SJP replay. CVC5 is optional and is used only when --cross-check-cvc5 is requested.
  • Initial distribution targets are Windows x64 and macOS Apple Silicon; other platforms are handled on request. The source snapshot does not include packaged releases or prove platform compatibility. See System Requirements.
  • The CLI does not expose a structured JSON diagnostics mode. Diagnostic text may change; scripts should rely on exit codes and documented result lines. See Diagnostics and Exit Codes.