Diagnostics and Exit Codes

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

This page documents the process status and output streams implemented by the CLI programs in that source snapshot. The codes describe command execution and proof outcomes; a generated artifact is not necessarily a successful proof.

Exit code summary

These meanings are not interchangeable across commands. In particular, make-sjv uses 0 to mean that it wrote an SJP, not that the proof recorded in it passed.

sekura-js

For check, ast, compile, and assemble, status 0 means the requested operation completed. Invalid arguments, invalid input, missing files, unsupported options, or processing errors return 1.

Examples of usage diagnostics include Unknown command, Missing file argument, check/ast expect a single file, Unsupported optimization level, and assemble does not support compile-only flags. Processing exceptions are printed with an Error: prefix. The CLI does not define a separate status for syntax errors or compiler errors; both return 1.

With no command, sekura-js prints its usage to standard error and returns 1. It has no --version option.

sekura-js also has compatibility entry points for SJV commands. Their statuses follow the sekura-sjv behavior below.

sekura-sjv inspection and model commands

parse, resolve, ast, and successful SJS verify-model return 0. Invalid input, missing files, parsing/resolution errors, or a failed model check return 1 and print an SJV error: diagnostic to standard error.

For an SJV selecting SystemVerilog, verify-model currently parses and elaborates the module and then returns 1 with a diagnostic that RTL-to-SMT translation is not implemented for that command. Use verify or make-sjv for the implemented SystemVerilog proof path.

sekura-sjv --help and -h print usage to standard output and return 0. Invoking it with no arguments prints the same usage and returns 1. Unknown commands and malformed command lines return 1.

sekura-sjv verify

SystemVerilog route

For verify <file.sjv> with a SystemVerilog source, return codes are:

A counterexample is also printed as COUNTEREXAMPLE name=value. Unsupported or inconclusive outcomes may include a DIAGNOSTIC line. A syntax/elaboration failure is an error, not a successful proof.

SJS/SOBJ route

For verify <file.sjv> <file.sobj> [environment.json]:

The functional/safety result lines are printed to standard output. Operational exceptions use the SOBJ verification error: prefix on standard error.

SJP commands

make-sjv

make-sjv returns 0 if it successfully writes the SJP. For SystemVerilog, the proof result is stored in the package and also reported; for SJS/SOBJ, assessment results are stored in it. A recorded FAILED, UNSUPPORTED, or INCONCLUSIVE result does not by itself make package generation return nonzero. A malformed input, unsupported command shape, or write/processing error returns 1 with an SJP error: diagnostic.

Automation must inspect the proof result as well as the process status. To require a usable proof artifact, follow generation with sign-sjp and verify-sjp; replay alone checks the stored obligations and does not regenerate them from source.

verify-sjp

The optional --cross-check-cvc5 adds a CVC5 replay requirement; a disagreement or unknown result prevents status 0. Z3 replay is performed regardless.

Key generation and signing

keygen-ed25519 and sign-sjp return 0 on success and 1 for invalid arguments, key/package errors, or file errors. Their caught errors use Key generation error: and SJP signing error: respectively.

Output streams

• sekura-js check prints Syntax OK to standard output; errors and usage diagnostics go to standard error.
• sekura-js compile prints compilation summaries to standard output. Lines such as Written: file.sobj are sent to standard error.
• SJV verification and SJP generation print progress/timing lines to standard error. Result lines, such as FUNCTIONAL PROVED, SJP WRITTEN, and SJP REPLAY MATCH, are printed to standard output.
• Usage and operational error diagnostics are generally written to standard error. Do not parse human-readable error text as a stable machine interface; use the process status and the command’s documented result line where one exists.

Shell and CI use

Check each command’s status immediately. When output is piped, enable the shell’s pipeline-failure handling (for example, set -o pipefail in Bash-compatible shells) so a failed CLI invocation is not hidden by a successful downstream command.

For proof gates, use a command whose exit status represents the proof outcome, or explicitly inspect both the status and result. Do not use make-sjv alone as a proof gate: status 0 confirms package creation only. A simple shell gate for SystemVerilog is:

sekura-sjv verify adder.sjv >verify.stdout 2>verify.stderr
status=$?
if [ "$status" -ne 0 ]; then
    cat verify.stderr >&2
    exit "$status"
fi

For SJP validation, gate on verify-sjp returning 0. Preserve stdout and stderr separately if CI needs to retain proof results and diagnostics as build artifacts.

Stability note

The numeric status classes above are implemented behavior, but most diagnostic strings are human-readable text and may change. The current CLI does not expose a structured JSON diagnostics mode. Consumers should use exit status and documented result lines rather than matching arbitrary error-message wording.