Sekura JS Generated Artifacts

This page describes files written by the implementation at SekuraJS source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236.

Documentation version: 1.0

1. Artifact overview

For the ordinary non-mono runtime-module path, sekura-js compile program.sjs writes four sibling files:

program.sjs
    │
    ├── sekura-js compile
    │      ├── program.sasm
    │      ├── program.sdef
    │      ├── program.sobj
    │      └── program.smod
    │
    └── sekura-sjv (separate verification command)
           └── program.sjp

sekura-js generates .sasm, .sdef, .sobj, and, for non-library runtime modules outside mono mode, .smod. SJP generation and signing belong to sekura-sjv; the compiler does not create an SJP. See the SJP format reference for the package’s internal structure.

2. .sasm — generated assembly text

The compiler translates SJS into textual Memora8 assembly and writes it as .sasm unless --final-only is selected. It is a compiler intermediate that can be inspected or passed to the separate assembler command:

sekura-js assemble program.sasm

assemble requires a matching .sdef file. It reads the assembly, assembles and links it, and writes .sobj.

3. .sdef — symbol and layout definition

The linker writes .sdef alongside .sobj unless --final-only is selected. It records the source name, page size, text base, data base, entry point (or none), function placements, and labels. sekura-js assemble reads the text_base and data_base values from this file and uses entry_point when present.

.sdef is separate from the executable object. The current linker source comments that symbol information is carried in the accompanying .sdef file.

4. .sobj — Memora8 executable object

.sobj is the binary object written by compilation unless --no-sobj is selected. sekura-js assemble also writes an .sobj from .sasm and .sdef.

The current writer emits a little-endian binary with a 28-byte header:

The header is followed by text words and then data words. Data is padded by one zero word when needed to meet the writer’s 8-byte data alignment rule. Although the linker API has an optional module-metadata page, the current sekura-js compile and assemble paths call it without that metadata argument; the generated SOBJ from these CLI paths therefore has no such page.

An SOBJ is an object for the Memora8/MR8 target. sekura-js writes it but does not execute it. Execution requires a separate runtime or simulator.

5. .smod — textual module interface metadata

For a non-mono, non-library runtime module, compilation writes a textual .smod file. The compiler also reads .smod files when resolving runtime-module imports and may reuse the current module’s .smod to recover the module name, RegID, and system-module marker.

The generated file may contain:

• module and regid records;
• the system marker for a system module;
• import aliases and imported module names;
• exported function names, IDs, and parameter counts;
• exported variables and constants with type and index;
• exported structure size and field type/offset records;
• runtime_data __module_runtime 512 0 when the generated module has runtime entry data.

Only exported declarations are written as interface records. A library module does not get .smod from the current compiler path. Mono mode also skips .smod generation.

6. How compile options change files written

--no-sobj and --final-only cannot be used together. These options control which files the current invocation writes; they do not delete files left by an earlier compilation. A stale .sasm, .sdef, .sobj, or .smod can remain in the directory if the selected mode no longer writes it.

For each input, output basenames are derived from the supplied path with a final .sjs removed. If the path has no .sjs suffix, the compiler reads <path>.sjs and uses <path> as the output basename.

7. Source files may be updated

During non-mono compilation of a runtime module, the compiler can generate a RegID. If the source has a named module declaration without an explicit RegID, the compiler attempts to write the generated or reused RegID into that source declaration. Thus a compile can modify its .sjs input as well as write build artifacts.

A source without an explicit module declaration receives a module name based on its filename; the compiler writes the module metadata to .smod for the regular runtime-module path.

8. .sjp — verification package from sekura-sjv

.sjp is created by sekura-sjv make-sjv (the make-sjp spelling is a legacy alias), not by sekura-js compile. Current SJS/SOBJ and SystemVerilog paths write SJP v2 ZIP packages. make-sjv writes an unsigned package; sekura-sjv sign-sjp writes a signed copy at a different output path.

The SJP package contains a manifest and captured SMT query payloads, and can contain embedded proof-dependency packages. verify-sjp requires the signed package and an explicit public key, then checks its signature and replays the stored obligations through Z3. The optional --cross-check-cvc5 option adds the CVC5 replay. Creating an SJP does not imply that its recorded proof result is successful; read the recorded results and replay outcome.

SJP is a user-created verification artifact. Its rights are governed by the relationships between its creator, user, and customer; creating it does not by itself make it a proprietary Sekura JS product artifact. See SJP Package Format and SJP Signatures.

9. Ed25519 key files

The separate sekura-sjv keygen-ed25519 command writes:

• the secret key as 64 raw bytes, with owner read/write permissions;
• the public key as 64 hexadecimal characters followed by a newline.

Both output paths must differ and must not already exist. These are key files supplied by the caller; they are not emitted by compilation or SJP generation. The secret key is used by sign-sjp; the public key is supplied to verify-sjp using --trusted-key.

10. Other files and temporary data

• .sjs and .sjv are source inputs; the compiler does not generate them.
• A verification environment JSON file is an optional input to SJS/SOBJ verification and SJP generation; it is not written by the tool.
• SJP’s manifest.json and .smt2 obligations are members inside the .sjp ZIP package, not separate persistent output files from make-sjv.
• Solver query files and temporary child packages are written under the system temporary directory during processing and removed by the current implementation after the solver or replay call.
• Build outputs and CLI test executables are CMake build products, not generated program artifacts.

11. References

• sekura-js CLI reference — compiler and assembler commands and output options.
• sekura-sjv CLI reference — SJV verification, SJP, and signing commands.
• SJP Package Format — package members, manifest, attestation, and replay checks.
• SJP Signatures — signing and key behavior.

Checked against src-js/main.cpp, src-js/linker_memora8.cpp, src-js/linker_memora8.h, src-sjv/cli/cli.cpp, and src-sjv/core/sjp.cpp at the source revision stated above. No tests or site build were run while preparing this page.