Sekura JS and SJV Examples

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

These examples describe implemented behavior in the source snapshot above. They assume the tools have been built or installed and that Z3 is available for proof and SJP replay. CVC5 is only needed for the optional cross-check.

1. Check and compile a Sekura JS module

The repository includes verification_identity.sjs, a small module with a u32 global and an identity function:

let r2: u32 = 0;

let identity(value: u32): u32 {
    return value;
}

Check its syntax and compile it:

sekura-js check examples/verification_identity.sjs
sekura-js compile examples/verification_identity.sjs

The syntax check prints Syntax OK. Compilation writes the generated .sasm, .sdef, .sobj, and .smod files beside the source. It does not execute the SOBJ; running it requires the separate MR8 simulator.

2. SJV and SJS/SOBJ example status

The paired verification_identity.sjv is useful for parser and model checks:

sekura-sjv parse examples/verification_identity.sjv
sekura-sjv verify-model examples/verification_identity.sjv

These commands check the SJV input and model. They do not establish that the compiled SOBJ implements the contract. In the current source test, implementation verification of this identity fixture reports FUNCTIONAL UNSUPPORTED because the return target cannot be proven. Do not treat this fixture as a passing SJS/SOBJ implementation proof.

The implemented SystemVerilog route below is a positive end-to-end proof example.

3. Prove a supported SystemVerilog function

Create adder.sv:

module adder;
  function automatic logic [7:0] add(input logic [7:0] a, input logic [7:0] b);
    begin
      add = a + b;
    end
  endfunction
endmodule

Create adder.sjv in the same directory:

module "adder.sv";

{ 1 == 1; }

function add {
    return' == a + b;
}

Run the proof:

sekura-sjv verify adder.sjv

For this example, the verifier reports FUNCTIONAL PROVED and exits with status 0. This is a direct proof of the supported SystemVerilog subset; the tool does not convert SystemVerilog into SOBJ.

To see a counterexample, change the contract to return' == a + b + 1;. The corresponding checked source test expects FUNCTIONAL COUNTEREXAMPLE and exit status 2.

4. Create, sign, and replay an SJP

From the directory containing the two adder files, generate an SJP:

sekura-sjv make-sjv adder.sjv adder.sjp

make-sjv creates an unsigned SJP v2 package. Package-generation success alone does not mean the recorded proof passed; inspect the result printed by the command.

Generate a keypair, sign to a new file, then verify the signed package:

sekura-sjv keygen-ed25519 signing.secret signing.public
sekura-sjv sign-sjp adder.sjp signing.secret adder.signed.sjp
sekura-sjv verify-sjp adder.signed.sjp --trusted-key signing.public

For the proved adder example, successful replay prints SJP REPLAY MATCH and exits with status 0. verify-sjp requires the signed package and the explicitly supplied public key. Keep signing.secret private; do not publish it with the example files.

To request the implemented optional second-solver check, add --cross-check-cvc5 to verify-sjp and make sure cvc5 is available on PATH:

sekura-sjv verify-sjp adder.signed.sjp --trusted-key signing.public --cross-check-cvc5

5. Boundaries of these examples

• sekura-js compile produces MR8 SOBJ and related files; it does not run them.
• verify-model checks an SJV model, not the compiled implementation.
• SJS/SOBJ implementation verification is a separate path and the checked-in identity fixture currently returns FUNCTIONAL UNSUPPORTED.
• The demonstrated SystemVerilog proof covers one supported combinational function; it does not imply general SystemVerilog support.
• make-sjv creates an unsigned package. Only a signed package with an explicit public key can pass verify-sjp.
• SJP replay checks the saved SMT obligations. It does not regenerate them from the original source files.

For complete command syntax and supported SystemVerilog constructs, see the SJV CLI reference, Getting Started, and SystemVerilog subset reference.