Integer Mode (--int-mode)

Current verified code uses checked integer semantics. The --int-mode flag exists, but the Viper verification lane rejects bitvec and unchecked today.

Syntax

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

For --verify and --viper, the only accepted mode is checked. Omitting the flag is equivalent to --int-mode checked.

Examples

# Checked mode (default) - prove no overflow/underflow
sector9 --verify --int-mode checked file.sr9

# Omit the flag for default checked behavior
sector9 --verify file.sr9

Current Verification Policy

Mode	Flag	Behavior
Checked	--int-mode checked	Overflow fails verification (default)
Bitvec	--int-mode bitvec	Rejected by --verify and --viper
Unchecked	--int-mode unchecked	Rejected by --verify and --viper

Checked Mode (Default)

In checked mode, the verifier generates proof obligations for each arithmetic operation on fixed-width types. Verification fails if an operation could overflow or underflow.

sector9 --verify file.sr9  # Checked is the default

You must provide preconditions that rule out overflow:

public func increment(x : Nat8) : async Nat8
  entry_requires x < 255;  // Runtime entry guard for exported callers
  requires x < 255;        // Without this, verification fails
  ensures result == x + 1;
{
  x + 1
}

Use checked mode for safety-critical code where overflows indicate bugs.

Rejected Modes

If you run verification or Viper emission with a non-checked mode, Sector9 fails before producing a usable Viper artifact:

sector9 --verify --int-mode bitvec file.sr9

The diagnostic states that verification requires --int-mode=checked.

When Each Mode Applies

The integer mode affects fixed-width types (Nat8, Nat16, Nat32, Nat64, Int8, Int16, Int32, Int64). Unbounded Nat and Int are always mathematical integers.

Fixed-Width Type Bounds

Type	Minimum	Maximum
Nat8	0	255
Nat16	0	65,535
Nat32	0	4,294,967,295
Nat64	0	18,446,744,073,709,551,615
Int8	-128	127
Int16	-32,768	32,767
Int32	-2,147,483,648	2,147,483,647
Int64	-9,223,372,036,854,775,808	9,223,372,036,854,775,807

Spec vs Runtime Behavior

In the verified lane, fixed-width runtime expressions generate bounds obligations, and spec expressions stay mathematical but must still prove bounds where fixed-width results are required.

Combining with Other Flags

With --viper

Export Viper code using the checked verification encoding:

sector9 --viper --int-mode checked file.sr9 > out.vpr

Use checked mode when generating Viper artifacts intended for verification. Non-checked modes are not currently available through --viper.

With --cores

Parallel verification with a specific integer mode:

sector9 --verify --int-mode checked --cores 4 file.sr9

With --verify-timeout-ms

Set a timeout for verification with bounds checking:

sector9 --verify --int-mode checked --verify-timeout-ms 60000 file.sr9

With --counterexample

Debug overflow failures by examining counterexamples:

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

The counterexample shows input values that cause overflow.

Error Handling

Invalid Mode

If you specify an unrecognized mode:

sector9 --verify --int-mode invalid file.sr9

The CLI prints:

sector9: --int-mode expects one of: unchecked|checked|bitvec

And exits with code 2.

Missing Overflow Preconditions (Checked Mode)

When verification fails due to potential overflow, the verifier reports an error at the arithmetic operation. Add preconditions to rule out overflow:

// Fails in checked mode
public func unsafe_add(x : Nat8, y : Nat8) : async Nat8 {
  x + y  // Error: potential overflow
}

// Passes in checked mode
public func safe_add(x : Nat8, y : Nat8) : async Nat8
  entry_requires x + y <= 255;
  requires x + y <= 255;
{
  x + y
}

Verification Impact

Checked mode intentionally adds proof obligations for fixed-width arithmetic. That is the current sound verification surface. If bounds proofs become too large, prefer widening intermediates, adding helper lemmas, or using unbounded Nat/Int in the verified core.

See Also

• Overflow Checking Modes for detailed examples
• Bounds Proofs for proving arithmetic in bounds
• Division Safety for non-zero divisor requirements

Summary

• --verify and --viper accept checked mode only
• Omit the flag or pass --int-mode checked
• Checked mode requires proving no overflow
• bitvec and unchecked are rejected by the Viper verification lane
• The flag is case-insensitive
• Invalid modes exit with code 2
• Unbounded Nat and Int are unaffected by this flag