Source Checking (--check)

Validate syntax, types, imports, and verifier-surface legality without SMT solving. This is the fast feedback command for development iteration.

The --check flag runs the front-end checking pipeline in whole-imported-world hygiene mode. It catches syntax errors, type errors, import issues, contract annotation issues, and verifier-surface restrictions without invoking the SMT solver. This makes it significantly faster than --verify while still validating that your code is well-formed.

Basic Usage

sector9 --check file.sr9

On success, the command exits silently with code 0. On failure, it prints diagnostic messages to stderr and exits with a non-zero code.

What --check Validates

The --check flag performs these validations:

1. Lexical analysis - Tokenizes source code
2. Syntax parsing - Builds the abstract syntax tree
3. Import resolution - Resolves all import declarations
4. Type inference - Infers types for all expressions
5. Type checking - Verifies type consistency
6. Contract parsing - Validates requires, ensures, and invariant syntax
7. Verification-surface constraints - Enforces rules like pure function restrictions, proof-only collection placement, and token shared-boundary shape

What --check Does NOT Do

• Does not generate Viper intermediate code
• Does not invoke the SMT solver
• Does not prove that contracts hold
• Does not compile to WebAssembly

For formal verification, use --verify instead.

--check vs --verify

Aspect	--check	--verify
Type checking	Yes	Yes
Contract parsing	Yes	Yes
SMT solving	No	Yes
Proof verification	No	Yes
Speed	Fast (seconds)	Slower (depends on complexity)
Use case	Development iteration	Pre-deployment validation

Use --check for rapid iteration during development. Use --verify when you need mathematical proof that contracts hold.

Common Flags

Combine --check with these flags for better diagnostics:

# Show source code in error messages
sector9 --check --print-source-on-error file.sr9

# Verbose output
sector9 --check -v file.sr9

# Treat warnings as errors
sector9 --check -Werror file.sr9

# Hide warnings
sector9 --check --hide-warnings file.sr9

# Report multiple syntax errors (error recovery mode)
sector9 --check --error-recovery file.sr9

# Resolve imports from a local package
sector9 --package core ./core/src --check file.sr9

Exit Codes

Code	Meaning
0	Success - all checks passed
1	Failure - syntax, type, or other errors detected
2	Invalid arguments - missing files or conflicting flags

Error Message Format

Error messages follow this format:

<file>:<line>:<col>: <category> <severity> [<code>], <message>

Example output for a type error:

counter.sr9:5:12: type error [M0026], unbound variable x

Common error codes you may encounter:

Code	Description
M0001	Syntax error
M0026	Unbound variable
M0029	Unbound type
M0059	Operator not defined for operand type
M0095	Return type mismatch
M0151	Missing field in object literal
M0360	Higher-order function must be pure or contract-typed

Use sector9 --explain M0026 to request a longer explanation for a diagnostic code when one is available. Use --json with verification commands when tooling needs structured proof diagnostics.

Typical Workflow

# 1. Rapid source checking during development
sector9 --package core ./core/src --check my_actor.sr9

# 2. Fix any source, import, or verifier-surface errors reported

# 3. When --check passes, run full verification
sector9 --package core ./core/src --verify my_actor.sr9

# 4. On verification success, proceed to deployment

IDE Integration

The --check flag is designed for IDE integration. Its fast execution time makes it suitable for:

• Save-on-check workflows
• Continuous type-checking in editors
• Pre-commit hooks
• Quick validation in CI pipelines before expensive verification

Warning Control

Control which warnings are shown or treated as errors:

# Disable specific warnings
sector9 --check -A M0240 file.sr9

# Enable specific warnings
sector9 --check -W M0145 file.sr9

# Treat specific warnings as errors
sector9 --check -E M0145 file.sr9

# List available warning codes
sector9 --warn-help

Summary

• --check validates syntax, types, imports, and verifier-surface legality without SMT solving
• Fast enough for interactive development workflows
• Catches errors early before expensive verification
• Combine with --print-source-on-error for better diagnostics
• Use --verify when you need formal proofs
• Add --package <name> <path> for source files that import local packages such as mo:core/...
• A top-level actor must be declared persistent actor in the current frontend; plain actor is rejected before verification.