sekura-sjv Command-Line Reference

This document describes the implementation at SekuraJS source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236.

Documentation version: 1.0

1. Help and command shape

sekura-sjv <command> <files> [options]

With no arguments, the program prints the command summary to standard output and exits with status 1. sekura-sjv --help and sekura-sjv -h print the same summary and exit with status 0. An unknown command returns status 1. There is no version command.

The commands are:

parse | resolve | verify-model | ast <file.sjv>
verify <file.sjv> <file.sobj> [environment.json]
verify <file.sjv> [SystemVerilog build options]
make-sjv <file.sjv> <file.sjp> [SystemVerilog build options]
make-sjv <file.sjv> <file.sobj> <file.sjp> [environment.json]
keygen-ed25519 <secret.key> <public.key>
sign-sjp <unsigned.sjp> <secret.key> <signed.sjp>
verify-sjp <file.sjp> --trusted-key public.key [--cross-check-cvc5]
build-verify <file.sjv>

SJV paths and artifact paths are passed as written; this CLI does not automatically append .sjv, .sobj, or .sjp extensions.

2. Read and inspect SJV

parse

sekura-sjv parse model.sjv

Parses an SJV file and prints its module name, state-block count, and function count. It does not resolve the selected implementation or run a proof. Returns 0 on success and 1 for invalid arguments, file errors, or parse errors.

resolve

sekura-sjv resolve model.sjv

Resolves the source selected by the SJV module declaration. For SJS it loads and reports counts for globals, structs, and functions. For SystemVerilog it parses and elaborates the selected module using default build configuration, then reports symbol and static-instance counts. It does not prove the SJV contracts. Returns 0 on success; failures return 1.

ast

sekura-sjv ast model.sjv

Prints the SJV module name and counts for states, functions, invariant alternatives, and transitions, then prints function rule counts. Returns 0 on success and 1 on invalid arguments or errors.

verify-model

sekura-sjv verify-model model.sjv

Checks the SJV model and its consistency. When the SJV selects SJS, it resolves the source and verifies the model using the SJS formal model. When the SJV selects SystemVerilog, the current command parses and elaborates the SV module but then returns an error stating that the RTL-to-SMT translation is not implemented for verify-model. Use verify or make-sjv for the implemented combinational RTL proof path. Returns 0 on successful SJS model verification and 1 on errors, including the SV limitation.

3. verify for SJS and SOBJ

sekura-sjv verify model.sjv program.sobj [environment.json]

The SJV must select an SJS source. Required inputs are the SJV and SOBJ. The optional third input is a verification environment JSON file; when omitted, no environment file is loaded. The command checks the SJV model and types against the selected SJS module, loads the SOBJ, and reports functional verification plus machine-safety results (memory, MMU, and stack ABI).

The SOBJ path is required by the current argument checks. The source code contains a derived sibling-SOBJ fallback, but the command rejects an omitted SOBJ argument before reaching it.

Return values:

Legacy build-verify

sekura-sjv build-verify model.sjv

This legacy spelling is dispatched through verify without an SOBJ argument. In the current implementation it can reach the SystemVerilog verification branch with default options. For an SJS-selected model, verification requires an explicit SOBJ and the legacy spelling fails with that requirement. Prefer verify with the explicit inputs shown above.

4. verify for SystemVerilog

The SJV module declaration selects the primary .sv source. The command uses the current combinational RTL proof implementation; it is not a general SystemVerilog simulator or full-language verifier.

sekura-sjv verify model.sjv [SystemVerilog build options]

No SOBJ or environment JSON is used on this route. If no options are given, the build configuration has the built-in define SYNTHESIS=1; there are no additional source files, include directories, or parameter overrides.

Supported build options (repeatable where applicable):

Paths in these options are resolved relative to the directory containing the SJV file when relative. The top source selected by the SJV is included automatically. The implementation expands include directives and preprocesses the combined source set before parsing and elaboration.

The command prints MODEL CHECKED, the selected module, and a FUNCTIONAL result. Result statuses are:

Unsupported constructs can produce status 1; parsing or elaboration alone is not reported as a successful proof.

5. Create an SJP with make-sjv

The command also accepts the legacy alias make-sjp; both spellings use the same handler.

SJS/SOBJ input

sekura-sjv make-sjv model.sjv program.sobj proof.sjp [environment.json]

Inputs: SJV, SOBJ, output SJP path, and optional environment JSON. The SJV must select SJS source. The command checks and assesses the model, records the input fingerprints and captured SMT queries, then writes an SJP v2 package. It writes the package and returns status 0 when processing succeeds even if the recorded functional or safety result is failed, unsupported, or inconclusive. Inspect the results in the generated package and run verify-sjp after signing it.

The output package from make-sjv is unsigned. make-sjv does not sign the package.

SystemVerilog input

sekura-sjv make-sjv model.sjv proof.sjp [SystemVerilog build options]

The SJV selects the primary .sv source; the same source/include/define/parameter options as the SV verify command are accepted. The command preprocesses, parses and elaborates the source, runs the current combinational RTL proof path, and writes an SJP v2 package containing the result and captured SMT queries. It returns 0 if package generation completes, including when the proof result recorded in the package is not VERIFIED. The generated package is unsigned.

For SystemVerilog proof dependencies, the parent SJV may select dependent child SJV/SJP packages as implemented in the verifier. For SJS/SOBJ, the command rejects SJV proof dependencies.

SJP follow-up commands

A generated unsigned package must be signed before it can pass verify-sjp:

sekura-sjv sign-sjp proof.sjp signing.secret signed-proof.sjp
sekura-sjv verify-sjp signed-proof.sjp --trusted-key signing.public

See SJP Package Format for exact container and replay behavior.

6. Generate and use Ed25519 keys

keygen-ed25519

sekura-sjv keygen-ed25519 signing.secret signing.public

Generates an Ed25519 keypair. The secret key is written as 64 raw bytes and restricted to owner read/write permissions. The public key is written as 64 hexadecimal characters followed by a newline. Both output paths must be distinct and must not already exist.

Returns 0 on success; key-generation and file errors return 1. Keep the secret key private; the public key is the value supplied to verify-sjp.

sign-sjp

sekura-sjv sign-sjp unsigned.sjp signing.secret signed.sjp

Accepts an unsigned SJP v2 ZIP package and a 64-byte binary Ed25519 secret key generated by keygen-ed25519. Writes a signed copy with attestation.json. The package must not already contain an attestation, and the output path must differ from the input path.

Returns 0 on success and 1 on invalid package/key, file errors, or signing errors. The legacy line-oriented SJP v1 format cannot be signed by this command.

7. verify-sjp

sekura-sjv verify-sjp proof.sjp --trusted-key signing.public [--cross-check-cvc5]

The public key option is required. The key file can contain 32 raw bytes or 64 hexadecimal digits. The command:

1. requires a signed SJP v2 ZIP package;
2. verifies the Ed25519 attestation and checks that the supplied key equals the key embedded in it;
3. checks the SJP container and manifest references;
4. replays each stored SMT query with Z3 and compares its result with the recorded result;
5. recursively replays included proof dependencies;
6. with --cross-check-cvc5, also invokes CVC5 for each query and requires the result to match.

The caller supplies the public key to use. The command does not maintain an identity registry or decide who is trusted. Child package attestations are checked cryptographically during replay, but the root --trusted-key is not compared with the child package keys.

Z3 is required for replay. CVC5 is invoked only when --cross-check-cvc5 is specified; cvc5 must then be available on PATH. The CVC5 invocation uses SMT-LIB2 mode and a 3000 ms limit. Z3 replay uses SMT-LIB2 mode with a three-second command timeout. The cross-check does not replace Z3 replay.

Return values:

SJP v1 contains no stored SMT payloads and is reported as not replayable (status 2). An unsigned package or absent --trusted-key is rejected as an operational/signature error (status 1).

8. Output streams and progress

Verification and SJP-generation commands print stage timing/progress messages to standard error. Their result lines and summaries are printed to standard output. Key and signing commands print a success line to standard output. Errors are printed to standard error.

9. Compatibility entry points

The compiler executable still dispatches the shared SJV CLI for compatibility:

sekura-js sjv <subcommand> ...
sekura-js sjv-ast <file.sjv>
sekura-js verify-model <file.sjv>

The standalone executable is sekura-sjv. In that executable, ast is accepted as a short spelling for the SJV AST command; sekura-js retains the separate sjv-ast spelling.

10. Implementation references

Checked against source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236:

• src-sjv/cli/main.cpp — standalone help and command normalization;
• src-sjv/cli/cli.cpp — command arguments, verification paths, SystemVerilog options, signatures, and exit codes;
• src-sjv/core/sjp.cpp — SJP creation, package parsing, solver replay, and optional CVC5 replay;
• tests/sjv_cli_test.cpp and tests/sjv_sv_test.cpp — CLI cases represented in the test source.

No tests or site build were run while preparing this reference.