Incremental Verification

Verifying only changed modules.

Full verification of a large codebase can take minutes or longer. Incremental verification skips unchanged modules to reduce CI cycle times while maintaining verification guarantees for modified code.

The Challenge

Verification time grows with codebase size. A project with 20 modules might take 5 minutes to verify fully. Running this on every commit wastes CI resources when most commits touch only 1-2 files.

Full verification:     20 modules × 15s average = 5 minutes
Incremental (2 files): 2 modules × 15s average = 30 seconds

The goal is to identify which modules actually need re-verification based on what changed.

Dependency-Based Verification

Sector9 provides --print-deps to list a file's imports:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --print-deps src/main.sr9

Output shows resolved import paths:

mo:core/Nat /path/to/core/Nat.sr9
./lib/Math /path/to/src/lib/Math.sr9
./lib/Token /path/to/src/lib/Token.sr9

Use this to build a dependency graph and determine what needs re-verification when a file changes. --print-deps reports direct imports for one entry file; reverse dependency tracking is something your CI script or build system owns. If your sources import mo:core, pass the same package arguments you use for normal verification, for example --package core ./core/src.

Implementing Incremental Verification

Basic Script

A minimal incremental verification script using git to detect changes:

#!/bin/bash
set -euo pipefail

# Get changed files since last successful verification
CHANGED=$(git diff --name-only HEAD~1 -- '*.sr9' '*.mo')

if [ -z "$CHANGED" ]; then
  echo "No verification-relevant changes"
  exit 0
fi

# Verify only changed files
FAILED=0
for file in $CHANGED; do
  if [ -f "$file" ]; then
    echo "Verifying $file..."
    if ! XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --verify --verify-timeout-ms 120000 "$file"; then
      FAILED=1
    fi
  fi
done

exit $FAILED

With Dependency Tracking

Changed files may affect their dependents. A more thorough approach verifies both changed files and anything that imports them:

#!/bin/bash
set -euo pipefail

# Files changed in this commit
CHANGED=$(git diff --name-only HEAD~1 -- '*.sr9' '*.mo')

# Find files that import any changed file
DEPENDENTS=""
for changed in $CHANGED; do
  # Search for imports of the changed module
  module_name=$(basename "${changed%.*}")
  importing=$(rg -l "import .*${module_name}" src -g '*.sr9' -g '*.mo' || true)
  DEPENDENTS="$DEPENDENTS $importing"
done

# Combine and deduplicate
TO_VERIFY=$(echo "$CHANGED $DEPENDENTS" | tr ' ' '\n' | sort -u | grep -v '^$')

for file in $TO_VERIFY; do
  if [ -f "$file" ]; then
    echo "Verifying $file..."
    XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --verify --verify-timeout-ms 120000 "$file"
  fi
done

Deterministic Output for Custom Caching

The --deterministic flag produces stable Viper output. You can build a project-local content-addressed cache around that output:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --deterministic contract.sr9

With deterministic mode:

• Identifiers use source-location hashes instead of sequential counters
• Anonymous types get names like anonRecord$3baa8f76 based on structure
• Declaration ordering is alphabetically sorted

This is not a CHASH product feature: current CHASH is used for code identity, token shared-boundary wiring, and token stable identity, not as an end-to-end verification cache key. If you build your own cache, include all inputs that can affect verification, not just the source file.

Hash-Based Cache

#!/bin/bash
set -euo pipefail

CACHE_DIR="${XDG_CACHE_HOME:-$HOME/.cache}/sector9/verify-cache"
mkdir -p "$CACHE_DIR"

verify_with_cache() {
  local file="$1"

  # Generate deterministic Viper output
  local vpr_output
  vpr_output=$(XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --viper --deterministic "$file" 2>/dev/null)

  # Hash the output
  local hash
  hash=$(echo "$vpr_output" | sha256sum | cut -d' ' -f1)

  # Check cache
  if [ -f "$CACHE_DIR/$hash" ]; then
    echo "Cache hit for $file (hash: ${hash:0:8}...)"
    return 0
  fi

  # Cache miss - run verification
  echo "Verifying $file..."
  if XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --verify --deterministic --verify-timeout-ms 120000 "$file"; then
    # Cache successful verification
    touch "$CACHE_DIR/$hash"
    return 0
  else
    return 1
  fi
}

for file in "$@"; do
  verify_with_cache "$file"
done

Cache Invalidation

The example cache is invalidated when the generated deterministic Viper text changes. It is not automatically invalidated for every semantic input unless you include those inputs in the key.

Explicitly clear the cache when:

• Upgrading Sector9 to a new version
• Changing verification flags globally
• Changing trusted libraries or solver/Silicon versions
• Debugging cache-related issues

rm -rf "${XDG_CACHE_HOME:-$HOME/.cache}/sector9/verify-cache"

GitHub Actions Example

A complete workflow with incremental verification:

name: Incremental Verify
on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
        with:
          fetch-depth: 2  # Need previous commit for diff

      - name: Cache verification results
        uses: actions/cache@v4
        with:
          path: ~/.cache/sector9/verify-cache
          key: verify-${{ runner.os }}-${{ hashFiles('**/*.sr9') }}
          restore-keys: |
            verify-${{ runner.os }}-

      - name: Install Sector9
        run: |
          # Your installation steps here

      - name: Get changed files
        id: changes
        run: |
          CHANGED=$(git diff --name-only HEAD~1 -- '*.sr9' '*.mo' | tr '\n' ' ')
          echo "files=$CHANGED" >> $GITHUB_OUTPUT

      - name: Verify changed files
        if: steps.changes.outputs.files != ''
        run: |
          for file in ${{ steps.changes.outputs.files }}; do
            if [ -f "$file" ]; then
              echo "Verifying $file..."
              ./bin/sector9 --package core ./core/src --verify --deterministic --verify-timeout-ms 120000 "$file"
            fi
          done
        env:
          XDG_CACHE_HOME: ~/.cache

When to Use Full Verification

Incremental verification is faster but not always sufficient:

Scenario	Recommendation
Regular commits	Incremental
Merge to main	Full verification
Release builds	Full verification
CI nightly builds	Full verification
Prelude/library changes	Full verification

Triggering Full Verification

Run full verification on protected branches:

- name: Full verification on main
  if: github.ref == 'refs/heads/main'
  run: |
    find src \( -name "*.sr9" -o -name "*.mo" \) -exec ./bin/sector9 --package core ./core/src --verify {} \;

Or when critical files change:

- name: Check for critical changes
  id: critical
  run: |
    if git diff --name-only HEAD~1 | grep -E '(prelude|base|core)'; then
      echo "full=true" >> $GITHUB_OUTPUT
    fi

- name: Full verification if critical
  if: steps.critical.outputs.full == 'true'
  run: ./scripts/verify-all.sh

Modular Verification Strategy

Incremental verification works best with modular code. When modules have clear contracts:

1. Changed module: Re-verify the implementation against its contracts
2. Callers: Don't need re-verification if contracts are unchanged
3. Dependencies: Don't need re-verification (their verification is independent)

This is the key insight: contracts form verification boundaries. A change inside a module doesn't affect its callers as long as the contract is unchanged.

Module A (changed internally, same contract)
   ↓ calls
Module B (no re-verification needed)

See Modular Verification for patterns that improve incrementality.

Parallel Incremental Verification

Combine incremental detection with parallel execution:

#!/bin/bash
set -euo pipefail

CHANGED=$(git diff --name-only HEAD~1 -- '*.sr9' '*.mo')

if [ -z "$CHANGED" ]; then
  echo "No changes to verify"
  exit 0
fi

# Verify in parallel
echo "$CHANGED" | xargs -P 4 -I {} \
  XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --verify --verify-timeout-ms 120000 {}

Or with GNU parallel for better job control:

echo "$CHANGED" | parallel -j 4 \
  'XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --verify --verify-timeout-ms 120000 {} && echo "OK: {}" || echo "FAIL: {}"'

Limitations

Incremental verification has trade-offs:

Not detected automatically:

• Changes outside your dependency graph scan
• Changes to external dependencies such as core or trusted libraries
• Sector9, Silicon, or solver upgrades that change verification behavior

Requires discipline:

• Developers must understand the dependency graph
• Cache invalidation needs manual management
• Full verification should still run periodically

Edge cases:

• Macro expansions or code generation may not track properly
• Changes to verification flags require cache clearing

Best Practices

Start simple: Basic change detection is better than no incremental verification.

Cache conservatively: When in doubt, re-verify. False negatives (missed bugs) are worse than wasted CI time.

Run full verification nightly: Catch anything incremental verification missed.

Monitor verification times: Track which modules are slow and prioritize modularization.

Version your cache key: Include Sector9 version in cache keys to invalidate on upgrades.

Document your strategy: Make it clear what triggers incremental vs full verification.

See Also

• Running Verification in CI - Basic CI integration
• Regression Prevention - Golden file testing
• Modular Verification - Code organization for incrementality
• Deterministic Mode - Reproducible output

Summary

• Incremental verification skips unchanged modules to reduce CI time
• Use git diff or similar to detect changed files
• Track dependencies to verify affected modules, not just changed files
• Enable --deterministic if you build content-addressed caching
• Hash deterministic Viper output plus toolchain, solver, and flag inputs before skipping verification
• Run full verification on merges to main, releases, and nightly builds
• Modular code with clear contracts improves incrementality
• Combine with parallel execution for additional speedup