Skip to main content

Deterministic Mode (--deterministic)

Produce reproducible Viper artifacts with stable identifiers and consistent ordering.

Syntax​

sector9 --verify --deterministic file.sr9
sector9 --verify --no-deterministic file.sr9
sector9 --viper --deterministic file.sr9

Default Behavior​

Deterministic mode is enabled by default when using --verify. You only need to specify the flag explicitly when:

  • Using --viper (to emit Viper code with stable names)
  • Overriding the default with --no-deterministic
# Deterministic is automatic with --verify
sector9 --verify file.sr9

# Explicit for --viper mode
sector9 --viper --deterministic file.sr9

# Override the default
sector9 --verify --no-deterministic file.sr9

What Deterministic Mode Controls​

Deterministic mode affects how the translator generates identifiers and orders declarations in the Viper output.

Identifier Generation​

Without deterministic mode, the translator uses sequential counters for anonymous types and temporary variables:

$anonRecord_1, $anonRecord_2, ...
$temp_0, $temp_1, ...

With deterministic mode, identifiers are computed from source locations and type fingerprints:

anonRecord$3baa8f76, anonRecord$a1c2d3e4, ...
x_7f8a9b0c, y_1e2f3a4b, ...

These hash-based names remain stable across multiple runs of the compiler, as long as the source code does not change.

Declaration Ordering​

Without deterministic mode, declarations appear in the order they were processed during compilation. This order can vary between runs due to hash table iteration order and other non-deterministic factors.

With deterministic mode, the following are sorted alphabetically by name:

  • Ghost state items (predicates, axioms)
  • Permission declarations
  • Invariant conjuncts
  • Future constructors

This ensures the same .vpr file is produced every time.

Use Cases​

Golden File Testing​

When maintaining expected output files (goldens), deterministic mode ensures the Viper output matches byte-for-byte:

# Generate expected output
sector9 --viper --deterministic file.sr9 > expected.vpr

# Later, verify output hasn't changed
sector9 --viper --deterministic file.sr9 > actual.vpr
diff expected.vpr actual.vpr

CI/CD Pipelines​

For reproducible builds in continuous integration:

# Consistent verification artifacts across CI runs
sector9 --verify --deterministic --json file.sr9

Combined with --json, this ensures both the verification result and any intermediate artifacts are reproducible.

Caching and Incremental Verification​

Deterministic identifiers enable content-addressed caching. When the Viper output hash matches a cached result, verification can be skipped:

# Generate Viper code
sector9 --viper --deterministic file.sr9 > file.vpr

# Compute hash for caching
sha256sum file.vpr

Verifying Determinism​

The test infrastructure includes a script to verify that output is deterministic:

./scripts/check-viper-determinism.sh file.sr9

This runs the translator twice and compares the output. Any difference indicates a determinism bug.

Combining with Other Flags​

With parallelization​

Deterministic mode works correctly with parallel verification:

sector9 --verify --deterministic --cores 4 file.sr9

The ordering guarantees are preserved regardless of how many cores are used.

With timeout​

For CI pipelines requiring both reproducibility and time limits:

sector9 --verify --deterministic --verify-timeout-ms 300000 file.sr9

With JSON output​

Structured output combined with reproducible artifacts:

sector9 --verify --deterministic --json file.sr9

With integer mode​

Use checked integer mode for deterministic verification artifacts:

sector9 --verify --deterministic --int-mode checked file.sr9

When to Disable Deterministic Mode​

In most cases, keep deterministic mode enabled (the default for --verify). Consider disabling it only when:

  • Debugging translator issues where sequential IDs are easier to follow
  • Comparing against older non-deterministic golden files during migration
sector9 --verify --no-deterministic file.sr9

Implementation Details​

Deterministic mode affects three subsystems:

  1. Name generation - Uses cryptographic hashing of source locations instead of counters
  2. Type fingerprinting - Anonymous types get names based on their structure
  3. Collection ordering - Ghost IR items are sorted alphabetically before emission

The source location includes file path, line, and column information, making identifiers stable within a project but potentially different if the same code is compiled from different paths.

Summary​

  • --deterministic produces reproducible Viper artifacts
  • Enabled by default with --verify
  • Use explicitly with --viper for stable output
  • Override with --no-deterministic when needed
  • Essential for golden file testing and CI pipelines
  • Works correctly with --cores, --json, and other flags