SJP Package Format: Current Implementation

This document describes the behavior implemented by sekura-sjv at source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236. It is an implementation description, not a promise of features beyond that revision.

Package version written by the current SJS/SOBJ and SystemVerilog flows: 2
File extension: .sjp

1. What verify-sjp verifies

verify-sjp performs these checks on an SJP v2 package:

  1. Requires an Ed25519 attestation and an explicitly supplied public key (--trusted-key). It checks that the key is the same as the public key embedded in the attestation, then verifies the signature.
  2. Reads the ZIP package, checks supported ZIP structure, entry paths, size limits, duplicate names, and each entry’s ZIP CRC-32.
  3. Parses manifest.json and re-runs each referenced SMT-LIB query with Z3. It compares the result with the recorded result and reports a match only when the solver result is not unknown.
  4. With --cross-check-cvc5, also runs each query through CVC5 and requires its result to match the recorded result.
  5. For embedded dependency packages, checks the recorded package SHA-256, selected module/SJV/contract/scope/parameter relationships, and recursively replays the child package. Any child attestations are cryptographically checked, but the root --trusted-key is not applied to child packages.

This replay checks the formulas stored in the package. It does not regenerate them from SJS, SJV, SOBJ, or SystemVerilog inputs. Although the manifest records input hashes and configuration metadata, verify-sjp has no original input files to compare against those values. Therefore replay alone does not establish that the stored formulas were correctly generated from a particular source revision.

2. Container members

SJP v2 is a ZIP/ZIP64 archive. The writer currently creates entries without compression. The reader accepts ZIP stored and deflate entries. A package produced without dependencies contains:

manifest.json
obligations/000001.smt2
obligations/000002.smt2
...

When proof dependencies are present, the writer also stores the referenced child packages at paths recorded in the manifest, under dependencies/. Signing adds:

attestation.json

The archive reader rejects encrypted entries, unsafe paths, duplicate member names, unsupported compression methods, entries exceeding its limits, CRC mismatches, and files not referenced by the manifest. The current maximum archive and expanded-content size is 2 GiB; the reader also limits the ZIP directory to 100,000 entries and recursive dependency nesting to 32 packages.

3. Manifest written by the current serializer

The top-level manifest.json emitted by the v2 writer contains:

  • format_version: numeric value 2.
  • producer: name is SJV; version is currently the literal unversioned-build.
  • target, module_type, semantics_version, and source_kind.
  • inputs: sjv_hash, source_hash, source_set_hash, sobj_hash, elaboration_hash, configuration_hash, module_parameters, environment_hash, and metadata_hash. Values that do not apply to the selected frontend may be empty.
  • contracts, bounds, proof_scope, and dependencies.
  • solver: name Z3, detected version (or unavailable), logic QF_AUFBV, and recorded timeout 2000 ms.
  • obligations: records containing id, scope, kind, smt_path, smt_sha256, contract, expected_solver_result, and producer_result.
  • results: status strings produced for the frontend’s scopes.

The exact values vary by frontend. The Sekura JS/SOBJ flow sets source_kind to sjs, target to MR8, and records hashes for the selected source, SJV, SOBJ, optional environment, and adjacent .sdef metadata when available. The SystemVerilog flow sets source_kind to systemverilog, target to MR8, and records source-set and elaboration hashes, module type, parameters, contracts, and dependencies where applicable.

The ZIP writer creates sequential obligation paths such as obligations/000001.smt2. Each obligation hash is SHA-256 of the exact stored payload bytes. The reader requires every manifest-referenced payload to exist, checks its SHA-256, and rejects duplicate references and unreferenced files. The manifest must include version 2, a non-empty obligations array, and valid results and proof_scope values. Each query must use a supported kind (proof, feasibility, or solver-query) and a recorded result of sat, unsat, or unknown; the two stored result fields must agree.

A scope listed in proof_scope must have result VERIFIED. For a scope called functional, the verifier also requires a replayed proof query with result unsat. Any query marked proof for a scope recorded as VERIFIED must replay as unsat. Each listed contract must have a replayed functional proof query with that contract and result unsat.

4. Signature and attestation

The sign-sjp command adds one attestation.json to an unsigned v2 ZIP package. It refuses an already signed package. The current attestation JSON contains:

  • attestation_version: 1;
  • algorithm: Ed25519;
  • context: Sekura SJP attestation v1;
  • key_id: sha256: followed by the SHA-256 of the 32-byte public key;
  • manifest_sha256: sha256: followed by the SHA-256 of the exact manifest bytes;
  • public_key_hex: the 32-byte public key in hexadecimal;
  • signature_hex: the detached Ed25519 signature in hexadecimal.

The signed message is the byte sequence Sekura SJP attestation v1, followed by a NUL byte, followed by the exact manifest.json bytes. The signature directly covers the manifest. The obligation and child-package hashes inside that manifest bind those payloads to it. The ZIP CRC-32 detects entry corruption but is not a cryptographic signature over the complete ZIP byte stream.

verify-sjp requires --trusted-key public.key; the key file may contain 32 raw bytes or 64 hexadecimal digits. It rejects unsigned packages, invalid signatures, and a supplied key that differs from the embedded public key. The tool checks key equality but does not decide organizational identity or maintain a trust store. The public key must be selected and supplied by the caller.

make-sjv currently writes the proof package before signing. To produce a package accepted by verify-sjp, sign that output with sign-sjp, then verify the signed file with the intended public key.

5. Solver replay

Z3 is always used for replay. The stored SMT-LIB payload is sent to the z3 executable in SMT-LIB2 mode, with a three-second command timeout. If --cross-check-cvc5 is supplied, CVC5 is also invoked with a three-second time limit; the replay adapter removes the Z3 timeout setting and optional (get-model) line before invoking CVC5.

For each query, the output reports the recorded result and the replayed Z3 result; when requested, it also reports the CVC5 result. A result of unknown is inconclusive and does not establish a match. A different result is a mismatch. Successful replay means the included formulas reproduce the recorded solver results under these configured invocations; it is not a proof that the frontend translation itself was correct.

6. Embedded SystemVerilog proof dependencies

The current SJP v2 writer can embed child SJP files for the SystemVerilog dependency flow. Each dependency record contains instance_path, module_type, sjp_path, sjp_sha256, sjv_hash, selected contracts, selected proof_scopes, parameters, and port_bindings.

Replay checks the child bytes against sjp_sha256, confirms the child’s module type and SJV hash, checks selected contract and scope names, requires selected scopes to have VERIFIED status, compares parameter sets when recorded, and recursively replays the child. For every selected contract it requires a replayed functional proof query with result unsat. Port bindings are recorded in the manifest; the replay code validates their data types but does not re-elaborate RTL or independently recompute those bindings.

SJV proof dependencies currently require a SystemVerilog parent module. The SJS/SOBJ make-sjv path rejects proof dependencies.

7. Legacy SJP v1

The implementation retains a line-oriented legacy v1 representation beginning with version=1 for compatibility APIs. It does not contain the SMT formulas needed for replay. verify-sjp reports legacy v1 as not replayable, and the signing path supports only v2 ZIP packages. The current public verifier workflow therefore requires a signed, replayable v2 package.

8. Commands

The relevant sekura-sjv commands are:

make-sjv <file.sjv> <file.sjp>                         (SystemVerilog)
make-sjv <file.sjv> <file.sobj> <file.sjp> [environment.json] (SJS/SOBJ)
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]

The make-sjp spelling is retained as a legacy alias for make-sjv.

9. Implementation references

This page was checked against the source revision identified above, especially:

  • src-sjv/core/sjp.cpp — v2 ZIP writer/reader, manifest generation, hashes, and replay;
  • src-sjv/cli/cli.cpp — key generation, signing, trusted-key check, CLI flow, and SJS/SOBJ and SystemVerilog package generation;
  • include/sekura/sjv/sjp.h — SJP data structures and API;
  • tests/sjv_cli_test.cpp and tests/sjv_sv_test.cpp — CLI/signature/replay scenarios represented in the test source.

No tests or site build were run while preparing this implementation description.